map_apply_eq_iff_map_symm_apply_eq

English

For a measurable equivalence f, κ.map f = η iff κ = η.map f^{-1}.

Русский

Для измеримого эквивалента f: κ.map f = η тогда κ = η.map f^{-1}.

LaTeX

$$$$ \\kappa.map f = \\eta \\iff \\kappa = \\eta.map f^{-1}. $$$$

Lean4

theorem map_apply_eq_iff_map_symm_apply_eq (κ : Kernel α β) {f : β ≃ᵐ γ} (η : Kernel α γ) :
    κ.map f = η ↔ κ = η.map f.symm := by
  simp_rw [Kernel.ext_iff, map_apply _ f.measurable, map_apply _ f.symm.measurable,
    f.map_apply_eq_iff_map_symm_apply_eq]

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