left_inv

Mathlib.CategoryTheory.Endofunctor.Algebra

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Endofunctor.Algebra.Initial.left_inv

English

Left_inv' implies left_inv; the left inverse of the initial structure is inverse to the identity.

Русский

Left_inv' означает left_inv; левый обратный начальной структуры является обратной к тождественному.

LaTeX

$$$\\text{left_inv'}(h) \\Rightarrow \\text{left_inv}(h)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru