union_null

Mathlib.MeasureTheory.Measure.NullMeasurable

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

English

If s is NullMeasurable Set and μ(t) = 0, then s ∪ t is NullMeasurable.

Русский

Если s — нулеизмеримое множество и μ(t) = 0, то s ∪ t — нулеизмеримо.

LaTeX

$$NullMeasurableSet s μ → μ t = 0 → NullMeasurableSet (s ∪ t) μ$$

Lean4

protected theorem union_null (hs : NullMeasurableSet s μ) (ht : μ t = 0) : NullMeasurableSet (s ∪ t) μ :=
  hs.union (of_null ht)

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

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

Разделы

Аффилиация

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