instPreorder — Mathlib

English

The space of continuous order-preserving maps α →Co β is equipped with a pointwise preorder: f ≤ g iff ∀ a, f a ≤ g a.

Русский

Множество отображений α →Co β подчинено покажному порядку: f ≤ g тогда и только тогда, когда ∀ a, f a ≤ g a.

LaTeX

$$$f \le g \;\Leftrightarrow\; \forall a, f(a) \le g(a)$$$

Lean4

instance : Preorder (α →Co β) :=
  Preorder.lift ((↑) : (α →Co β) → α → β)

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