OAI/Probability/CriticalPercolation/Gluing/MoveExit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SimpleGraph.Walk.bounded_first_crossing line 20
2. def OAI.CriticalPercolation.BondGraph.axisExit line 57
3. lemma OAI.CriticalPercolation.BondGraph.axisExit_upper line 61
4. lemma OAI.CriticalPercolation.BondGraph.axisExit_finiteWitness line 63
5. lemma OAI.CriticalPercolation.BondGraph.axisExit_measurable line 66
6. lemma OAI.CriticalPercolation.BondGraph.axisExit_iff line 70
7. lemma OAI.CriticalPercolation.BondGraph.axisExit_of_crossing line 86
8. lemma OAI.CriticalPercolation.BondGraph.favored_of_union line 111