ae_restrict_mem

Mathlib.MeasureTheory.Measure.Restrict

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

English

If s is measurable, then (ae μ).mem of s is included in ae μ|_s

Русский

Если s измеримо, то множество a.e. ξ в μ принадлежит s включается в a.e. по μ|_s

LaTeX

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

Lean4

theorem ae_restrict_mem (hs : MeasurableSet s) : ∀ᵐ x ∂μ.restrict s, x ∈ s :=
  ae_restrict_mem₀ hs.nullMeasurableSet

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

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

Разделы

Аффилиация

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