measure_closure_of_null_frontier — Mathlib

English

μ(frontier s) = 0 implies closure s and s are almost everywhere equal.

Русский

Если frontier s имеет нулевую меру, то closure s и s равны почти всюду.

LaTeX

$$$\\text{closure}_{ae}\\, s = s$ при $\\mu(\\operatorname{frontier}(s)) = 0$.$$

Lean4

theorem measure_closure_of_null_frontier {μ : Measure α'} {s : Set α'} (h : μ (frontier s) = 0) : μ (closure s) = μ s :=
  measure_congr (closure_ae_eq_of_null_frontier h)

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