instPreorder — Mathlib

English

TopHom α β inherits a preorder from α → β by pointwise order: f ≤ g iff f(a) ≤ g(a) for all a.

Русский

TopHom α β наследует предорядок от функций α → β, задаваемый точечным образом: f ≤ g ⇔ ∀a, f(a) ≤ g(a).

LaTeX

$$$f \\le g \\;\\text{ iff }\\; \\forall a, f(a) \\le g(a).$$$

Lean4

instance [Preorder β] [Top β] : Preorder (TopHom α β) :=
  Preorder.lift (DFunLike.coe : TopHom α β → α → β)

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