isIso_op_iff

Mathlib.CategoryTheory.Opposites

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

English

For any morphism f, f.op is an isomorphism iff f is an isomorphism.

Русский

Для любой морфизмы f, f.op изоморфизм тогда и только тогда, когда f изоморфизм.

LaTeX

$$IsIso f.op \Leftrightarrow IsIso f$$

Lean4

theorem isIso_op_iff {X Y : C} (f : X ⟶ Y) : IsIso f.op ↔ IsIso f :=
  ⟨fun _ => isIso_of_op _, fun _ => inferInstance⟩

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

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

Разделы

Аффилиация

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