English
Let C be a category. For any objects X, Y in the opposite category C^{op} and any morphism f: X → Y that is an isomorphism in C^{op}, the underlying morphism f^{unop}: Y^{unop} → X^{unop} is an isomorphism in C.
Русский
Пусть C — категория. Пусть X, Y — объекты в противоположной категории C^{op} и f: X → Y — изоморфизм в C^{op}. Тогда f^{unop}: Y → X является изоморфизмом в C.
LaTeX
$$$\\\\forall C [\\\\text{Category}(C)], \\\\forall X,Y \in \mathrm{Obj}(C^{\\\\mathrm{op}}), \\\\forall f: X \to Y, \\\\text{IsIso}(f) \\\\Rightarrow \\\\text{IsIso}(f^{\\\\mathrm{unop}}).$$$
Lean4
instance isIso_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : IsIso f.unop :=
(isIso_unop_iff _).2 inferInstance
