measure_restrict_compl

Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms

URI: https://scilib.ai/kg/mathlib#Set.Countable.measure_restrict_compl

← MathLib Explorer

English

If s is countable, restricting μ to sᶜ leaves μ unchanged.

Русский

Если s счётно, ограничение μ на отношение к sᶜ не изменяет μ.

LaTeX

$$$$\mu|_{s^c} = \mu \quad\text{when } s\text{ is countable}.$$$$

Lean4

theorem _root_.Set.Countable.measure_restrict_compl (h : s.Countable) (μ : Measure α) [NoAtoms μ] : μ.restrict sᶜ = μ :=
  restrict_eq_self_of_ae_mem <| h.ae_notMem μ

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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