inv_eq_inv

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsIso.inv_eq_inv

English

For isomorphisms f,g, inv f = inv g iff f = g.

Русский

Для изоморфизмов f,g сопоставимо inv f = inv g ↔ f = g.

LaTeX

$$$inv\ f = inv\ g \iff f = g$$$

Lean4

theorem inv_eq_inv {f g : X ⟶ Y} [IsIso f] [IsIso g] : inv f = inv g ↔ f = g :=
  Iso.inv_eq_inv (asIso f) (asIso g)

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

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

Разделы

Аффилиация

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