OAI/Probability/LatticeSurface/Coercivity/OuterHulls.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SparseHoles.outerHulls line 18
  2. lemma OAI.SparseHoles.outer_mem line 24
  3. lemma OAI.SparseHoles.hull_subset_outer line 30
  4. lemma OAI.SparseHoles.outer_origin line 39
  5. structure OAI.SparseHoles.ClusterFamily line 43
  6. lemma OAI.SparseHoles.outer_disjoint line 49
  7. lemma OAI.SparseHoles.outer_rim_good line 65
  8. lemma OAI.SparseHoles.outer_separated line 78
  9. lemma OAI.SparseHoles.rim_nonempty line 88
  10. theorem OAI.SparseHoles.outer_hull_geometry line 98