Ico_ae_eq_Icc'

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

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

Русский

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

LaTeX

$$Ico_ae_eq_Ioc' (hb : μ { b } = 0) : Ico a b =ᵐ[μ] Ioc a b$$

Lean4

theorem Ico_ae_eq_Icc' (hb : μ { b } = 0) : Ico a b =ᵐ[μ] Icc a b :=
  (ae_eq_refl _).inter (Iio_ae_eq_Iic' hb)

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

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

Разделы

Аффилиация

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