OAI/Combinatorics/ContingencyTables/Rooted/RootedCut.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The explicit endpoint on the side away from a selected root

One reachability test in the edge-deleted forest selects the endpoint. No choice of a component representative or of a cut vertex is needed.

  1. def OAI.ContingencyTables.RootedCut.away line 20
  2. def OAI.ContingencyTables.RootedCut.cut line 23
  3. theorem OAI.ContingencyTables.RootedCut.away_properties line 26
  4. theorem OAI.ContingencyTables.RootedCut.selected_nonroot line 53
  5. def OAI.ContingencyTables.RootedCut.treeCut line 68
  6. lemma OAI.ContingencyTables.RootedCut.treeCut_self line 72
  7. lemma OAI.ContingencyTables.RootedCut.treeCut_nonroot line 76
  8. def OAI.ContingencyTables.RootedCut.sign line 80
  9. lemma OAI.ContingencyTables.RootedCut.sign_abs_self line 84
  10. lemma OAI.ContingencyTables.RootedCut.sign_self_ne_zero line 88
  11. lemma OAI.ContingencyTables.RootedCut.sign_abs_le_one line 95
  12. lemma OAI.ContingencyTables.RootedCut.other_tree_sign_zero line 101