op_monotone_iff

Mathlib.CategoryTheory.ObjectProperty.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.op_monotone_iff

English

For object properties P, Q on C, P.op ≤ Q.op if and only if P ≤ Q.

Русский

Для свойств объектов P и Q над C выполнено: P.op ≤ Q.op тогда и только тогда, когда P ≤ Q.

LaTeX

$$$P^{\mathrm{op}} \le Q^{\mathrm{op}} \iff P \le Q$$$

Lean4

@[simp]
theorem op_monotone_iff {P Q : ObjectProperty C} : P.op ≤ Q.op ↔ P ≤ Q :=
  ⟨unop_monotone, op_monotone⟩

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

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

Разделы

Аффилиация

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