comp_left_iff — Mathlib

English

For a measurable equivalence e and a function g, composing on the left with e is equivalent to composing on the right with e, in the sense of measure-preserving maps.

Русский

Для измеримого эквивалента e и функции g композиция слева с e эквивалентна композиции справа с e в понятии сохранения меры.

LaTeX

$$$hf: MeasurePreserving e μ_b μ_c \\Rightarrow (MeasurePreserving (e \\circ g) μ_a μ_c) \\Leftrightarrow (MeasurePreserving g μ_a μ_b)$$$

Lean4

protected theorem comp_left_iff {g : α → β} {e : β ≃ᵐ γ} (h : MeasurePreserving e μb μc) :
    MeasurePreserving (e ∘ g) μa μc ↔ MeasurePreserving g μa μb :=
  by
  refine ⟨fun hg => ?_, fun hg => h.comp hg⟩
  convert (MeasurePreserving.symm e h).comp hg
  simp [← Function.comp_assoc e.symm e g]

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