of_null

Mathlib.MeasureTheory.Measure.NullMeasurable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.NullMeasurableSet.of_null

English

If μ(s) = 0, then s is null-measurable with respect to μ.

Русский

Если μ(с) = 0, тогда множество с является нулево-измеримым по μ.

LaTeX

$$$$ \\mu(s) = 0 \\Rightarrow \\text{NullMeasurableSet } s \\ μ. $$$$

Lean4

theorem of_null (h : μ s = 0) : NullMeasurableSet s μ :=
  ⟨∅, MeasurableSet.empty, ae_eq_empty.2 h⟩

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

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

Разделы

Аффилиация

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