symm_mk — Mathlib

English

Two measurable equivalences are equal if they have the same underlying function.

Русский

Два измеримых эквивалента равны, если их подлежащие функции совпадают.

LaTeX

$$$$ \forall e_1,e_2: \alpha \simeq_m \beta,\ (e_1 : \alpha \to \beta) = e_2 \Rightarrow e_1 = e_2. $$$$

Lean4

@[simp]
theorem symm_mk (e : α ≃ β) (h1 : Measurable e) (h2 : Measurable e.symm) :
    (⟨e, h1, h2⟩ : α ≃ᵐ β).symm = ⟨e.symm, h2, h1⟩ :=
  rfl

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