inv_comp_eq_id

Mathlib.CategoryTheory.Iso

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

English

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

Русский

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

LaTeX

$$$inv\ g\gg f = 𝟙 X\iff f = g$$$

Lean4

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

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

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

Разделы

Аффилиация

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