instPartialOrder — Mathlib

English

Assume R has a partial order. The order on C(X,R)₀ is defined pointwise: f ≤ g iff ∀ x, f(x) ≤ g(x).

Русский

Пусть у R есть частичный порядок. Порядок на C(X,R)₀ задаётся по точкам: f ≤ g тогда и только тогда, когда для всех x выполняется f(x) ≤ g(x).

LaTeX

$$$ f \\le g \\iff \\forall x,\\ f(x) \\le g(x) $$$

Lean4

instance instPartialOrder [PartialOrder R] : PartialOrder C(X, R)₀ :=
  .lift _ DFunLike.coe_injective'

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