isIso_unop_iff — Mathlib

English

For f : X ⟶ Y in the opposite category, f.unop is an isomorphism iff f is an isomorphism.

Русский

Для f : X ⟶ Y в противоположной категории, f.unop изоморфизм тогда и только тогда, когда f изоморфизм.

LaTeX

$$IsIso f.unop \Leftrightarrow IsIso f$$

Lean4

theorem isIso_unop_iff {X Y : Cᵒᵖ} (f : X ⟶ Y) : IsIso f.unop ↔ IsIso f := by
  rw [← isIso_op_iff f.unop, Quiver.Hom.op_unop]

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