trim_eq_map — Mathlib

English

The trimmed measure μ.trim hm equals the pushforward of μ by the identity map: μ.trim hm = map id μ.

Русский

Обрезанная мера μ.trim hm равна отображению меры μ по тождественному отображению: μ.trim hm = map id μ.

LaTeX

$$$μ\\text{.trim}(hm) = μ\\text{.map}(id).$$$

Lean4

theorem trim_eq_map (hm : m ≤ m0) : μ.trim hm = @Measure.map _ _ _ m id μ :=
  by
  refine @Measure.ext α m _ _ (fun s hs ↦ ?_)
  rw [Measure.map_apply (measurable_id'' hm) hs, trim_measurableSet_eq hm hs, Set.preimage_id]

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