comp_inv_eq_id

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.comp_inv_eq_id

English

For α: X ⟶ Y an isomorphism, g = inv α ≫ f iff α ≫ g = f.

Русский

Для изomорфизма α: X ⟶ Y, g = inv α ≫ f эквивалентно α ≫ g = f.

LaTeX

$$$g = inv\ α\gg f\iff α\gg g = f$$$

Lean4

theorem comp_inv_eq_id (g : X ⟶ Y) [IsIso g] {f : X ⟶ Y} : f ≫ inv g = 𝟙 X ↔ f = g :=
  (asIso g).comp_inv_eq_id

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

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

Разделы

Аффилиация

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