restrict_Iio_eq_restrict_Iic

Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms

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

English

The measures μ restricted to Iio a and Iic a are equal when μ has no atoms.

Русский

Меры, ограниченные множествами Iio a и Iic a, равны, если μ без атомов.

LaTeX

$$\mu|_{Iio a} = \mu|_{Iic a}$$

Lean4

theorem restrict_Iio_eq_restrict_Iic : μ.restrict (Iio a) = μ.restrict (Iic a) :=
  restrict_congr_set Iio_ae_eq_Iic

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

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

Разделы

Аффилиация

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