OAI/Probability/CriticalPercolation/Clusters/ClusterObject.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CriticalPercolation.BondGraph.ClusterObject line 19
2. def OAI.CriticalPercolation.BondGraph.clusterObject line 21
3. def OAI.CriticalPercolation.BondGraph.eraseVertices line 24
4. lemma OAI.CriticalPercolation.BondGraph.incidentEdges_mono line 26
5. lemma OAI.CriticalPercolation.BondGraph.clusterObject_mono line 30
6. lemma OAI.CriticalPercolation.BondGraph.eraseVertices_mono line 35
7. lemma OAI.CriticalPercolation.BondGraph.eraseVertices_antitone line 39
8. lemma OAI.CriticalPercolation.BondGraph.openGraph_eraseVertices line 43
9. lemma OAI.CriticalPercolation.BondGraph.eraseVertices_dependsOn line 63
10. lemma OAI.CriticalPercolation.BondGraph.clusterObject_eq_of_incident line 72
11. lemma OAI.CriticalPercolation.BondGraph.dependsOn_exact_clusterObject line 90
12. lemma OAI.CriticalPercolation.BondGraph.roots_disjoint_symm line 98
13. lemma OAI.CriticalPercolation.BondGraph.roots_disjoint_roots line 107
14. lemma OAI.CriticalPercolation.BondGraph.roots_erase_roots line 114
15. lemma OAI.CriticalPercolation.BondGraph.openBond_roots line 128
16. lemma OAI.CriticalPercolation.BondGraph.clusterObject_erase_other line 137
17. lemma OAI.CriticalPercolation.BondGraph.clusterObject_exposure line 156
18. lemma OAI.CriticalPercolation.BondGraph.clusterObject_avoidance_exposure line 169