instPreorder — Mathlib

English

The order on the set of order-homomorphisms is defined pointwise by evaluation at each point: f ≤ g iff ∀x, f x ≤ g x.

Русский

Порядок на множестве отображений, сохраняющих порядок, задаётся по точке: f ≤ g тогда и только тогда, когда для всех x выполняется f(x) ≤ g(x).

LaTeX

$$$\\forall f,g:\\alpha \\to_o \\beta,\\; f \\le g \\iff \\forall x:\\alpha,\\; f(x) \\le g(x).$$$

Lean4

/-- The preorder structure of `α →o β` is pointwise inequality: `f ≤ g ↔ ∀ a, f a ≤ g a`. -/
instance : Preorder (α →o β) :=
  @Preorder.lift (α →o β) (α → β) _ toFun

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