map_congr — Mathlib

English

For a scalar c, (c · μ).map f = c · (μ.map f).

Русский

Для скаляра c выполнено: (c · μ).map f = c · (μ.map f).

LaTeX

$$$ (c \cdot \mu).map f = c \cdot (\mu.map f) $$$

Lean4

theorem map_congr {f g : α → β} (h : f =ᵐ[μ] g) : Measure.map f μ = Measure.map g μ :=
  by
  by_cases hf : AEMeasurable f μ
  · have hg : AEMeasurable g μ := hf.congr h
    simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hg]
    exact mapₗ_congr hf.measurable_mk hg.measurable_mk (hf.ae_eq_mk.symm.trans (h.trans hg.ae_eq_mk))
  · have hg : ¬AEMeasurable g μ := by simpa [← aemeasurable_congr h] using hf
    simp [map_of_not_aemeasurable, hf, hg]

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