OAI/Geometry/RCD/Coordinates/OpenRegularCutoff.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_open_regular_cutoff line 18

   Source documentation

   Every compact subset of an open set admits a compact Lipschitz plateau with an actual L² weak Laplacian. Finite unions of the RCD ball cutoffs supply the arbitrary shape without an additional analytic hypothesis.

   theorem NoncollapsedRCD.exists_open_regular_cutoff {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
       {Ω S : Set X} (hΩ : IsOpen Ω) (hS : IsCompact S) (hsub : S ⊆ Ω) :
       letI := locallyFinite_of_finiteOnBounded (hausdorff n X) hX.finiteOnBounded
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.locallyFinite_of_finiteOnBounded, OAI.RegularPointCoordinates.hausdorff