OAI/Probability/LatticeSurface/Coercivity/HullRims.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SparseHoles.mem_rim_iff_star line 17
2. lemma OAI.SparseHoles.disjoint_hulls_rim line 25
3. lemma OAI.SparseHoles.disjoint_hulls_separated line 38
4. lemma OAI.SparseHoles.exterior_independent line 50
5. lemma OAI.SparseHoles.filled_independent line 73
6. lemma OAI.SparseHoles.filled_in_any_box line 80