unop_monotone — Mathlib

English

Let P and Q be object properties on the opposite category Cᵒᵖ. If P ≤ Q, then applying the unop operation yields P.unop ≤ Q.unop.

Русский

Пусть P и Q — свойства объектов в противоположной категории Cᵒᵖ. Если P ⊆ Q, то P.unop ⊆ Q.unop.

LaTeX

$$$P \le Q \Rightarrow P^{\mathrm{unop}} \le Q^{\mathrm{unop}}$$$

Lean4

theorem unop_monotone {P Q : ObjectProperty Cᵒᵖ} (h : P ≤ Q) : P.unop ≤ Q.unop := fun _ hX ↦ h _ hX

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