inv_isIso

Mathlib.CategoryTheory.Iso

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

English

If f is an isomorphism, then inv f is also an isomorphism.

Русский

Если f — изоморфизм, то inv f — тоже изоморфизм.

LaTeX

$$IsIso (inv f)$$

Lean4

instance inv_isIso [IsIso f] : IsIso (inv f) :=
  (asIso f).isIso_inv

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

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

Разделы

Аффилиация

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