OAI/Probability/CriticalPercolation/Gluing/CollarDistance.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.vertexCollar line 15
2. def OAI.CriticalPercolation.BondGraph.distanceTo line 17
3. lemma OAI.CriticalPercolation.BondGraph.vertexCollar_exists line 20
4. lemma OAI.CriticalPercolation.BondGraph.distanceTo_mem line 26
5. lemma OAI.CriticalPercolation.BondGraph.distanceTo_le line 31
6. lemma OAI.CriticalPercolation.BondGraph.distanceTo_le_iff line 37
7. lemma OAI.CriticalPercolation.BondGraph.distanceTo_eq_zero_iff line 47
8. lemma OAI.CriticalPercolation.BondGraph.distanceTo_adj line 52
9. lemma OAI.CriticalPercolation.BondGraph.distanceTo_ball line 58
10. lemma OAI.CriticalPercolation.BondGraph.distanceTo_predecessor line 73