trans_eq_refl_iff_eq_symm — Mathlib

English

For f: α ≃ β and g: β ≃ α, f.trans g = Refl α iff f = g.symm.

Русский

Для f: α ≃ β и g: β ≃ α, f.trans g = тождество α тогда и только тогда, когда f = g.symm.

LaTeX

$$$ f.trans g = \mathrm{Id}_α \iff f = g^{-1} $$

Lean4

theorem trans_eq_refl_iff_eq_symm {f : α ≃ β} {g : β ≃ α} : f.trans g = Equiv.refl α ↔ f = g.symm := by
  rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]

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