OAI/Probability/CriticalPercolation/Gluing/FreshExitWitness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.freshExitEvent line 16
2. lemma OAI.CriticalPercolation.BondGraph.freshClusterBoundary_induced_mono line 20
3. lemma OAI.CriticalPercolation.BondGraph.freshExitEvent_upper line 37
4. lemma OAI.CriticalPercolation.BondGraph.freshExitEvent_finiteWitness line 43
5. lemma OAI.CriticalPercolation.BondGraph.measurableSet_freshExitEvent line 73
6. lemma OAI.CriticalPercolation.BondGraph.freshExitEvent_of_card line 78