unmop_inj

Mathlib.CategoryTheory.Monoidal.Opposite

URI: https://scilib.ai/kg/mathlib#Quiver.Hom.unmop_inj

English

For all f, g: X^op ⟶ Y^op, unmop f = unmop g implies f = g.

Русский

Для любых f, g: X^op ⟶ Y^op, unmop f = unmop g значит f = g.

LaTeX

$$$$ \\forall f,g:\\,X^{\\mathrm{op}}\\to Y^{\\mathrm{op}},\\; \\mathrm{unmop}(f) = \\mathrm{unmop}(g) \\Rightarrow f = g $$$$

Lean4

theorem unmop_inj {X Y : Cᴹᵒᵖ} : Function.Injective (Quiver.Hom.unmop : (X ⟶ Y) → (unmop' X ⟶ unmop' Y)) := fun _ _ H =>
  congr_arg Quiver.Hom.mop H

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

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

Разделы

Аффилиация

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