Iio_ae_eq_Iic

Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Iio_ae_eq_Iic

English

For all a, the intervals Iio a and Iic a coincide μ-almost everywhere when μ has no atoms.

Русский

Для всякого a의 множества Iio a и Iic a совпадают μ-почти повсеместно при отсутствии атомов μ.

LaTeX

$$Iio a =_{\mu-\text{a.e.}} Iic a$$

Lean4

theorem Iio_ae_eq_Iic : Iio a =ᵐ[μ] Iic a :=
  Iio_ae_eq_Iic' (measure_singleton a)

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

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

Разделы

Аффилиация

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