unmop_inj_iff

Mathlib.CategoryTheory.Monoidal.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalOpposite.unmop_inj_iff

English

For all x, y in C^op, unmop x = unmop y if and only if x = y.

Русский

Для любых x, y в C^op верно: unmop x = unmop y тогда и только если x = y.

LaTeX

$$$$ (unmop\,x = unmop\,y) \\iff (x = y) $$$$

Lean4

@[simp]
theorem unmop_inj_iff (x y : Cᴹᵒᵖ) : unmop x = unmop y ↔ x = y :=
  unmop_injective.eq_iff

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

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

Разделы

Аффилиация

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