hom_inv_id — Mathlib

English

If f is an isomorphism, then f followed by its inverse equals the identity on the source: f ∘ f^{-1} = id_X.

Русский

Если f — изоморфизм, то композиция f с её обратной даёт тождественное отображение на источнике: f ∘ f^{-1} = id_X.

LaTeX

$$$f \circ f^{-1} = \mathrm{id}_X$$$

Lean4

@[simp, grind =]
theorem hom_inv_id (f : X ⟶ Y) [I : IsIso f] : f ≫ inv f = 𝟙 X :=
  (Classical.choose_spec I.1).left

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