measureReal_restrict_apply₀ — Mathlib

English

If t is NullMeasurable with respect to μ restricted to s, then the real-valued measure of (μ|s) on t equals μ.real (t ∩ s).

Русский

Пусть t является нулепромежуточно измеримым относительно меры μ, ограниченной на s; тогда (μ|s).real(t) = μ.real(t ∩ s).

LaTeX

$$$ (\\mu \\restriction s).real t = \\mu.real (t \\cap s) $$$

Lean4

theorem measureReal_restrict_apply₀ (ht : NullMeasurableSet t (μ.restrict s)) :
    (μ.restrict s).real t = μ.real (t ∩ s) := by simp only [measureReal_def, restrict_apply₀ ht]

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