OAI/Probability/BenjaminiSchramm/GhostFan.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Percolation.BenjaminiSchramm.GhostFan line 11
2. lemma OAI.Percolation.BenjaminiSchramm.GhostFan.symm line 14
3. lemma OAI.Percolation.BenjaminiSchramm.walk_edges_disjoint_of_single_support_intersection line 18
4. lemma OAI.Percolation.BenjaminiSchramm.ghostFan_of_trail_support line 29
5. lemma OAI.Percolation.BenjaminiSchramm.ghostFan_of_first_arm_support line 36
6. lemma OAI.Percolation.BenjaminiSchramm.ghostFan_of_arm_avoiding_prefix line 45
7. lemma OAI.Percolation.BenjaminiSchramm.GhostFan.of_alternate_walk line 64
8. lemma OAI.Percolation.BenjaminiSchramm.GhostFan.of_not_isBridge line 102
9. lemma OAI.Percolation.BenjaminiSchramm.exists_bridge_to_ghostFan line 109
10. lemma OAI.Percolation.BenjaminiSchramm.walk_edges_disjoint_of_bridge line 131
11. lemma OAI.Percolation.BenjaminiSchramm.bridge_to_ghostFan_avoids_marks line 148
12. lemma OAI.Percolation.BenjaminiSchramm.GhostFan.mono line 182
13. lemma OAI.Percolation.BenjaminiSchramm.ghostFan_delete_bridge line 188
14. lemma OAI.Percolation.BenjaminiSchramm.two_connections_fan_or_bridge line 213