trim_trim — Mathlib

English

Trimming twice is the same as trimming once with the composed refinement: (μ.trim hm2).trim hm12 = μ.trim (hm12.trans hm2).

Русский

Дважды обрезка эквивалентна обрезке ровно одной: (μ.trim hm2).trim hm12 = μ.trim (hm12.trans hm2).

LaTeX

$$$(μ.trim hm_2).trim hm_{12} = μ.trim (hm_{12}.trans hm_2).$$$

Lean4

theorem trim_trim {m₁ m₂ : MeasurableSpace α} {hm₁₂ : m₁ ≤ m₂} {hm₂ : m₂ ≤ m0} :
    (μ.trim hm₂).trim hm₁₂ = μ.trim (hm₁₂.trans hm₂) :=
  by
  refine @Measure.ext _ m₁ _ _ (fun t ht => ?_)
  rw [trim_measurableSet_eq hm₁₂ ht, trim_measurableSet_eq (hm₁₂.trans hm₂) ht, trim_measurableSet_eq hm₂ (hm₁₂ t ht)]

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