restrict_Ioo_eq_restrict_Icc

Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms

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

English

The measures μ restricted to Ioo a b and Icc a b are equal when μ has no atoms.

Русский

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

LaTeX

$$\mu|_{Ioo a b} = \mu|_{Icc a b}$$

Lean4

theorem restrict_Ioo_eq_restrict_Icc : μ.restrict (Ioo a b) = μ.restrict (Icc a b) :=
  restrict_congr_set Ioo_ae_eq_Icc

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

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

Разделы

Аффилиация

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