OAI/Probability/UnimodularPercolation/Encounter/TreeBranches.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Tree branches, cluster retractions and terminal connecting trees.

  1. theorem OAI.Percolation.cutVertex_le_deleteEdge line 18
  2. theorem OAI.Percolation.tree_cut_neighbors line 29
  3. theorem OAI.Percolation.cut_reachable_self_eq line 43
  4. theorem OAI.Percolation.tree_branch_contains_leaf line 51
  5. theorem OAI.Percolation.pruned_tree_branch_marked line 105
  6. theorem OAI.Percolation.tree_three_leaves_branch line 115
  7. theorem OAI.Percolation.pruned_tree_three_branches line 135
  8. theorem OAI.Percolation.exists_cluster_retraction line 168
  9. theorem OAI.Percolation.glued_cut_conn line 188
  10. theorem OAI.Percolation.glued_conn line 213
  11. def OAI.Percolation.terminalGraph line 231
  12. theorem OAI.Percolation.terminalGraph_touch line 243
  13. theorem OAI.Percolation.terminalGraph_leaf line 251
  14. theorem OAI.Percolation.terminalGraph_connected line 260
  15. theorem OAI.Percolation.exists_terminal_tree line 284