partialOrder — Mathlib

English

If β has a partial order, then there is a canonical pointwise partial order on C(α, β): f ≤ g iff ∀ a, f(a) ≤ g(a).

Русский

Если β имеет частичный порядок, то на C(α,β) задаётся канонический по точкам частичный порядок: f ≤ g тогда и только тогда, когда для каждого a выполняется f(a) ≤ g(a).

LaTeX

$$\$PartialOrder \\beta) \\Rightarrow PartialOrder (C(α, β))\$ with $f ≤ g \\iff ∀ a, f(a) ≤ g(a)$.$$

Lean4

instance partialOrder [PartialOrder β] : PartialOrder C(α, β) :=
  PartialOrder.lift (fun f => f.toFun) (fun f g _ => by aesop)

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