partialOrder — Mathlib

English

Define a pointwise partial order on C_c(α,β) induced by the partial order on β; i.e., f ≤ g iff f(a) ≤ g(a) for all a ∈ α.

Русский

Определим покомпонентно упорядочение: f ≤ g тогда и только тогда, когда f(a) ≤ g(a) для всех a ∈ α.

LaTeX

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

Lean4

instance partialOrder : PartialOrder C_c(α, β) :=
  PartialOrder.lift (⇑) DFunLike.coe_injective

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