Ioo_ae_eq_Ico'

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Ioo_ae_eq_Ico'

English

If μ({a}) = 0 and μ({b}) = 0, then Ioo(a,b) =ᵐ μ Icc(a,b).

Русский

Если μ({a}) = 0 и μ({b}) = 0, то Ioo(a,b) совпадает с Icc(a,b) почти по μ.

LaTeX

$$Ioo_ae_eq_Icc' (ha : μ { a } = 0) (hb : μ { b } = 0) : Ioo a b =ᵐ[μ] Icc a b$$

Lean4

theorem Ioo_ae_eq_Ico' (ha : μ { a } = 0) : Ioo a b =ᵐ[μ] Ico a b :=
  (Ioi_ae_eq_Ici' ha).inter (ae_eq_refl _)

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

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

Разделы

Аффилиация

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