unop_monotone_iff

Mathlib.CategoryTheory.ObjectProperty.Opposite

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

English

For object properties P, Q on Cᵒᵖ, P.unop ≤ Q.unop if and only if P ≤ Q.

Русский

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

LaTeX

$$$P.unop \le Q.unop \iff P \le Q$$$

Lean4

@[simp]
theorem unop_monotone_iff {P Q : ObjectProperty Cᵒᵖ} : P.unop ≤ Q.unop ↔ P ≤ Q :=
  ⟨op_monotone, unop_monotone⟩

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

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

Разделы

Аффилиация

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