op_monotone

Mathlib.CategoryTheory.ObjectProperty.Opposite

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

English

Same as above: monotonicity of taking opposites of morphism properties.

Русский

То же самое: монотонность взятия противоположности свойств морфизмов.

LaTeX

$$$P \le Q \Rightarrow P^{op} \le Q^{op}$$$

Lean4

theorem op_monotone {P Q : ObjectProperty C} (h : P ≤ Q) : P.op ≤ Q.op := fun _ hX ↦ h _ hX

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

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

Разделы

Аффилиация

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