instPartialOrder — Mathlib

English

If β has a partial order, then α →Co β inherits a (pointwise) partial order, since each coordinate is ordered; this defines a partial order on continuous order-preserving maps.

Русский

Если β имеет частичный порядок, то множество α →Co β inherits точечный частичный порядок; это определяет частичный порядок на отображениях, сохраняющих порядок.

LaTeX

$$$[PartialOrder\;β] \Rightarrow\ PartialOrder (α \toCo β)$$$

Lean4

instance [PartialOrder β] : PartialOrder (α →Co β) :=
  PartialOrder.lift ((↑) : (α →Co β) → α → β) DFunLike.coe_injective

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