symm_trans_self — Mathlib

English

The symmetric (inverse) of a measurable equivalence, composed with itself, is the identity on the codomain.

Русский

Симметрическая (обратная) часть измеримого эквивалента, умноженная на саму себя, даёт идентичность на кодомене.

LaTeX

$$$$ e^{-1} \circ e = \mathrm{id}. $$$$

Lean4

@[simp]
theorem symm_trans_self (e : α ≃ᵐ β) : e.symm.trans e = refl β :=
  ext e.self_comp_symm

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