symm_comp_self_toHom — Mathlib

English

For any L-structure M and N, the map f ↦ toFunLike.coe f is bijective on L-equivalences.

Русский

Для любых структур M,N над языком L отображение f ↦ toFunLike.coe f является биективным на L-эквивалентностях.

LaTeX

$$$\forall f : M \cong_L N,\; \operatorname{Bijective}(\operatorname{toFunLike}(f))$$$

Lean4

@[simp]
theorem symm_comp_self_toHom (f : M ≃[L] N) : f.symm.toHom.comp f.toHom = Hom.id L M := by
  rw [← comp_toHom, symm_comp_self, refl_toHom]

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