nullMeasurableSet_Ico — Mathlib

English

Let α be a space with a topology and μ a measure. Then the half‑open interval Ico(a,b) is null‑measurable with respect to μ; equivalently there exists a measurable set E with μ(E Δ Ico(a,b)) = 0.

Русский

Пусть α имеет топологию и μ — мера. Тогда полузакрытый интервал Ico(a,b) является нуль‑измеримым по отношению к μ; то есть существует измеримое множество E такое, что μ(E Δ Ico(a,b)) = 0.

LaTeX

$$$\exists E\, (MeasurableSet\ E \land \mu(E \triangle \ Ico(a,b)) = 0)$$$

Lean4

theorem nullMeasurableSet_Ico : NullMeasurableSet (Ico a b) μ :=
  measurableSet_Ico.nullMeasurableSet

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