OAI/Probability/CriticalPercolation/GraphTopology/GraphNeighborhoodCompact.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.GraphTopology.reachBall line 14
2. lemma OAI.CriticalPercolation.GraphTopology.reachBall_self line 17
3. lemma OAI.CriticalPercolation.GraphTopology.reachBall_symm line 20
4. lemma OAI.CriticalPercolation.GraphTopology.reachBall_add line 25
5. lemma OAI.CriticalPercolation.GraphTopology.reachBall_finite line 31
6. lemma OAI.CriticalPercolation.GraphTopology.iso_reachBall line 49
7. lemma OAI.CriticalPercolation.GraphTopology.inverse_displacement line 54
8. lemma OAI.CriticalPercolation.GraphTopology.compact_displacement line 62
9. lemma OAI.CriticalPercolation.GraphTopology.compact_stabilizer line 78
10. lemma OAI.CriticalPercolation.GraphTopology.open_displacement line 88
11. lemma OAI.CriticalPercolation.GraphTopology.open_stabilizer line 91
12. lemma OAI.CriticalPercolation.GraphTopology.locallyCompact_aut line 94
13. instance OAI.CriticalPercolation.GraphTopology.aut_totallyDisconnected line 100
14. lemma OAI.CriticalPercolation.GraphTopology.compact_finite_vertex_images line 104