unop_inj — Mathlib

English

Taking opposites on arrows is injective: if unop f = unop g for arrows f,g: X ⟶ Y in the opposite category, then f = g.

Русский

Переобразование стрелок через операцию unop инъективно: если unop f = unop g для стрелок f,g: X→Y в противоположной категории, то f = g.

LaTeX

$$$\text{unop}$ инъективно: если $f,g: X\to Y$ в противоположной категории и $\mathrm{unop}(f)=\mathrm{unop}(g)$, то $f=g$$$

Lean4

theorem unop_inj {X Y : Cᵒᵖ} : Function.Injective (Quiver.Hom.unop : (X ⟶ Y) → (Opposite.unop Y ⟶ Opposite.unop X)) :=
  fun _ _ H => congr_arg Quiver.Hom.op H

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