restrict_Ioi_eq_restrict_Ici

Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms

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

English

The measures μ restricted to Ioi a and Ici a are equal when μ has no atoms.

Русский

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

LaTeX

$$\mu|_{Ioi a} = \mu|_{Ici a}$$

Lean4

theorem restrict_Ioi_eq_restrict_Ici : μ.restrict (Ioi a) = μ.restrict (Ici a) :=
  restrict_congr_set Ioi_ae_eq_Ici

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

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

Разделы

Аффилиация

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