ae_restrict_eq_bot

Mathlib.MeasureTheory.Measure.Restrict

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

English

For a measurable set s, s is a member of the a.e. content of μ.restrict s.

Русский

Для измеримого множества s, s принадлежит a.e.-содержимому μ|_s.

LaTeX

$$$\text{MeasurableSet}(s) \Rightarrow s \in \ae(μ|_s).$$$

Lean4

theorem ae_restrict_eq_bot {s} : ae (μ.restrict s) = ⊥ ↔ μ s = 0 :=
  ae_eq_bot.trans restrict_eq_zero

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

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

Разделы

Аффилиация

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