restrict_apply₀ — Mathlib

English

Restriction is monotone in the set and in the measure: if s is almost everywhere contained in s' with respect to μ and μ ≤ ν, then μ|s ≤ ν|s'.

Русский

Ограничение монотонно по множествам и по самой мере: если s содержится в s' почти везде относительно μ, и μ ≤ ν, то μ|s ≤ ν|s'.

LaTeX

$$$(\text{ae } μ).\text{EventuallyLE}(s, s') \rightarrow μ|s ≤ ν|s'.$$$

Lean4

theorem restrict_apply₀ (ht : NullMeasurableSet t (μ.restrict s)) : μ.restrict s t = μ (t ∩ s) := by
  rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply, coe_toOuterMeasure]

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