toHom_comp_symm_toHom — Mathlib

English

For an isomorphism f, the composition f.symm.toHom ∘ f.toHom equals the identity on graphs.

Русский

Для изоморфизма f композиция f.symm.toHom ∘ f.toHom равна тождественному отображению на графе.

LaTeX

$$$ f.symm.toHom \circ f.toHom = \mathrm{Hom.id} $$$

Lean4

@[simp]
theorem toHom_comp_symm_toHom : f.toHom.comp f.symm.toHom = Hom.id :=
  by
  ext v
  simp only [RelHom.comp_apply, RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding, RelIso.apply_symm_apply,
    RelHom.id_apply]

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