out

Mathlib.MeasureTheory.Measure.NullMeasurable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.IsComplete.out

English

If h is μ.IsComplete, then for every s with μ(s)=0, s is measurable.

Русский

Если μ полна, то любой μ-нулевой множество измерим.

LaTeX

$$$(h:\mu.IsComplete) \Rightarrow \forall s,\; \mu s = 0 \rightarrow \mathrm{MeasurableSet}(s).$$$

Lean4

theorem out (h : μ.IsComplete) : ∀ s, μ s = 0 → MeasurableSet s :=
  h.1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru