unop — Mathlib

English

If X is zero in C, then Opposite.unop X is zero in C.

Русский

Если X нулевой в Cᵒᵖ, то Opposite.unop X нулевой в C.

LaTeX

$$$\\\\text{IsZero}(X) \\\\Rightarrow \\\\text{IsZero}(\\\\mathrm{Opposite}.\\\\mathrm{unop} X)$$$

Lean4

theorem unop {X : Cᵒᵖ} (h : IsZero X) : IsZero (Opposite.unop X) :=
  ⟨fun Y => ⟨⟨⟨(h.from_ (Opposite.op Y)).unop⟩, fun _ => Quiver.Hom.op_inj (h.eq_of_tgt _ _)⟩⟩, fun Y =>
    ⟨⟨⟨(h.to_ (Opposite.op Y)).unop⟩, fun _ => Quiver.Hom.op_inj (h.eq_of_src _ _)⟩⟩⟩

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