inv_hom_id — Mathlib

English

If f is an isomorphism, then inv f followed by f equals the identity on the target: inv f ∘ f = id_Y.

Русский

Если f — изоморфизм, то обратная к f затем f даёт тождественный отображение на мишени: inv f ∘ f = id_Y.

LaTeX

$$$\mathrm{inv}(f) \circ f = \mathrm{id}_Y$$$

Lean4

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

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