restrict_compl_singleton

Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms

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

English

For NoAtoms μ, μ.restrict ({a})ᶜ = μ.

Русский

Для μ без атомов, ограничение до комплемента единичного множества не изменяет меру.

LaTeX

$$$$\mu|_{\{a\}^c} = \mu.$$$$

Lean4

@[simp]
theorem restrict_compl_singleton (a : α) : μ.restrict ({ a }ᶜ) = μ :=
  (countable_singleton _).measure_restrict_compl μ

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

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

Разделы

Аффилиация

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