OAI/Probability/UnimodularPercolation/Encounter/Geometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Cut vertices and connected branches.

  1. def OAI.Percolation.cutVertex line 17
  2. def OAI.Percolation.branchCount line 22
  3. theorem OAI.Percolation.walk_reachable_cut line 25
  4. theorem OAI.Percolation.branchCount_le_degree line 38
  5. theorem OAI.Percolation.connected_erase_leaf line 64
  6. theorem OAI.Percolation.exists_pruned_connector line 82
  7. theorem OAI.Percolation.sum_branchCount_le line 112