eq_of_inv_eq_inv

Mathlib.CategoryTheory.Iso

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

← MathLib Explorer

English

If inv f = inv g for morphisms f,g with f,g iso, then f = g.

Русский

Если inv f = inv g для изоморфизмов f,g, то f = g.

LaTeX

$$$inv\ f = inv\ g\to f = g$$$

Lean4

theorem eq_of_inv_eq_inv {f g : X ⟶ Y} [IsIso f] [IsIso g] (p : inv f = inv g) : f = g :=
  by
  apply (cancel_epi (inv f)).1
  rw [inv_hom_id, p, inv_hom_id]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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