restrict_singleton'

Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.restrict_singleton'

English

Restriction to any set preserves the NoAtoms property.

Русский

Ограничение на произвольное множество сохраняет отсутствие атомов.

LaTeX

$$$$\text{If } [NoAtoms(\mu)], \text{ then } NoAtoms(\mu|_s).$$$$

Lean4

theorem restrict_singleton' {a : α} : μ.restrict { a } = 0 := by simp only [measure_singleton, Measure.restrict_eq_zero]

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

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

Разделы

Аффилиация

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