OAI/Probability/CriticalPercolation/Gluing/LevelContactGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.exteriorCluster line 19
2. def OAI.CriticalPercolation.BondGraph.levelContacts line 22
3. def OAI.CriticalPercolation.BondGraph.contactDrop line 25
4. lemma OAI.CriticalPercolation.BondGraph.contactDrop_subset_incident line 28
5. lemma OAI.CriticalPercolation.BondGraph.contactDrop_disjoint_exterior line 33
6. lemma OAI.CriticalPercolation.BondGraph.exteriorCluster_subset_level line 39
7. lemma OAI.CriticalPercolation.BondGraph.cluster_eq_exterior_of_drop_closed line 49
8. def OAI.CriticalPercolation.BondGraph.minimumLevel line 76
9. lemma OAI.CriticalPercolation.BondGraph.minimumLevel_of_drop_closed line 79
10. lemma OAI.CriticalPercolation.BondGraph.minimumLevel_pairwiseDisjoint line 94
11. lemma OAI.CriticalPercolation.BondGraph.measurableSet_minimumLevel line 103