OAI/Probability/CriticalPercolation/GraphGeometry/BallCutGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.ballCut line 18
2. lemma OAI.CriticalPercolation.BondGraph.ballCut_endpoints line 20
3. lemma OAI.CriticalPercolation.BondGraph.ballCut_subset_incident_sphere line 29
4. lemma OAI.CriticalPercolation.BondGraph.ballCut_finite line 35
5. lemma OAI.CriticalPercolation.BondGraph.ballCut_endpoints_mem line 40
6. lemma OAI.CriticalPercolation.BondGraph.ballCut_pairwise_disjoint line 48
7. lemma OAI.CriticalPercolation.BondGraph.ballCut_card_le line 63
8. lemma OAI.CriticalPercolation.BondGraph.cluster_subset_ball_of_closed_ballCut line 71
9. lemma OAI.CriticalPercolation.BondGraph.frequently_small_increments_of_linear_scales line 79
10. lemma OAI.CriticalPercolation.BondGraph.frequently_small_spheres_of_linear_scales line 101