right_inv — Mathlib

English

StrInv(h) is a left inverse to A.str, hence A.str is an isomorphism with StrInv as inverse.

Русский

StrInv(h) является левым обратным к A.str; следовательно A.str является изоморфизмом с StrInv в качестве обратной.

LaTeX

$$$\text{IsTerminal}(A) \Rightarrow (\text{strInv}(h) \circ A.str) = \mathrm{id}_{F(A.V)}$$$

Lean4

theorem right_inv : A.str ≫ strInv h = 𝟙 _ :=
  congr_arg Hom.f (right_inv' h)

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