mop_inj

Mathlib.CategoryTheory.Monoidal.Opposite

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

English

For all f, g: X ⟶ Y, if mop f = mop g then f = g.

Русский

Для любых f, g: X ⟶ Y, если mop f = mop g, то f = g.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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