instPreorder — Mathlib

English

There is a natural Preorder on BotHom α β defined by evaluation: f ≤ g iff ∀ a, f a ≤ g a.

Русский

Существует естественный предорядок на BotHom α β, задаваемый по значению: f ≤ g тогда и только тогда, когда ∀ a, f a ≤ g a.

LaTeX

$$$\text{Preorder} (\text{BotHom } \alpha \beta) \\ (f \le g \iff \forall a, f a \le g a)$$$

Lean4

instance [Preorder β] [Bot β] : Preorder (BotHom α β) :=
  Preorder.lift (DFunLike.coe : BotHom α β → α → β)

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