OAI/Probability/LatticeSurface/Coercivity/HullMore.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SparseHoles.safe_mono line 16
2. lemma OAI.SparseHoles.exterior_walk line 21
3. lemma OAI.SparseHoles.filled_mono_hull line 28
4. lemma OAI.SparseHoles.filled_boundary line 40
5. lemma OAI.SparseHoles.safe_step_small line 47
6. lemma OAI.SparseHoles.filled_rim_subset line 60
7. lemma OAI.SparseHoles.star_mem_constant line 80
8. lemma OAI.SparseHoles.cluster_dichotomy line 102
9. lemma OAI.SparseHoles.filled_laminar line 115