symm_trans_self — Mathlib

English

The composition of the inverse and the map equals the identity on the codomain.

Русский

Сложение объединение обратного и отображения даёт тождественное отображение на целевом пространстве.

LaTeX

$$$\forall e : X \simeq^{\mathrm{d}} Y,\ e^{\mathrm{symm}} \circ e = \mathrm{refl}(Y)$$$

Lean4

@[simp]
theorem symm_trans_self (e : X ≃ᵈ Y) : e.symm.trans e = refl Y :=
  DilationEquiv.ext e.apply_symm_apply

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