closure_ae_eq_of_null_frontier — Mathlib

English

If frontier s has measure zero, then μ(closure(s)) = μ(s).

Русский

Если граница s имеет нулевую меру, то μ(closure(s)) = μ(s).

LaTeX

$$$\\mu(\\operatorname{frontier}(s)) = 0 \\Rightarrow \\mu(\\overline{s}) = \\mu(s).$$$

Lean4

theorem closure_ae_eq_of_null_frontier {μ : Measure α'} {s : Set α'} (h : μ (frontier s) = 0) : closure s =ᵐ[μ] s :=
  ((ae_le_set.2 h).trans interior_subset.eventuallyLE).antisymm <| subset_closure.eventuallyLE

Похожие утверждения