Ico_ae_eq_Ioc'

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

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

Русский

Если μ({a}) = 0 и μ({b}) = 0, то Ioc(a,b) =ᵐ μ Icc(a,b).

LaTeX

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

Lean4

theorem Ico_ae_eq_Ioc' (ha : μ { a } = 0) (hb : μ { b } = 0) : Ico a b =ᵐ[μ] Ioc a b :=
  (Ioo_ae_eq_Ico' ha).symm.trans (Ioo_ae_eq_Ioc' hb)

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

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

Разделы

Аффилиация

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