instPartialOrder — Mathlib

English

If β has a partial order, then α →o β inherits a partial order via pointwise comparison of functions and extensionality for equality.

Русский

Если β обладает частичным порядком, то α →o β наследует частичный порядок точечным сравнением функций и эктенсионализмом равенства.

LaTeX

$$$\\text{PartialOrder}(\\alpha \\to_o \\beta)$ with $f \\le g$ iff $f.toFun \\le g.toFun$ and equality given by ext.$$

Lean4

instance {β : Type*} [PartialOrder β] : PartialOrder (α →o β) :=
  @PartialOrder.lift (α →o β) (α → β) _ toFun ext

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