map_measurableEquiv_injective — Mathlib

English

The map μ ↦ μ.map e, induced by a MeasurableEquiv e, is injective on measures.

Русский

Отображение мер в их перенесённые по эквиваленту меру является инъективным.

LaTeX

$$$$\\forall e:\\alpha \\simeq\\beta,\\; \\mathrm{Injective}(\\mathrm{Measure.map}\\ e).$$$$

Lean4

theorem map_measurableEquiv_injective (e : α ≃ᵐ β) : Injective (Measure.map e) :=
  by
  intro μ₁ μ₂ hμ
  apply_fun Measure.map e.symm at hμ
  simpa [map_symm_map e] using hμ

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