nullMeasurableSet_of_null_frontier

English

There exists a measurable set with frontier of measure zero, hence null measurable.

Русский

Существует измеримое множество с нулевой мерой границы, следовательно ноль-измеримо.

LaTeX

$$$\\text{NullMeasurableSet}(s, \\mu)$ whenever $\\mu(\\operatorname{frontier}(s)) = 0$.$$

Lean4

theorem nullMeasurableSet_of_null_frontier {s : Set α} {μ : Measure α} (h : μ (frontier s) = 0) :
    NullMeasurableSet s μ :=
  ⟨interior s, isOpen_interior.measurableSet, (interior_ae_eq_of_null_frontier h).symm⟩

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