measureReal_restrict_apply₀'

Mathlib.MeasureTheory.Measure.Real

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measureReal_restrict_apply₀'

English

If s is NullMeasurable with respect to μ, then μ.restrict s t = μ(t ∩ s).

Русский

Пусть s - нулевизмеримо относительно μ, тогда μ.restrict s t = μ(t ∩ s).

LaTeX

$$$ \\mu.restrict s t = \\mu (t \\cap s) $$$

Lean4

theorem measureReal_restrict_apply₀' (hs : NullMeasurableSet s μ) : μ.restrict s t = μ (t ∩ s) := by
  simp only [restrict_apply₀' hs]

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

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

Разделы

Аффилиация

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