partialOrder — Mathlib

English

If α and β have partial orders, then the Lex construction on their sum carries a natural partial order, combining componentwise comparisons with Lex rules.

Русский

Если есть частичные порядки на α и β, то конструктор Lex на их сумме задаёт естественный частичный порядок, сочетающий по компонентам и лексикографическое правило.

LaTeX

$$$\\text{PartialOrder}(\\,\\alpha \\oplus_ℓ \\beta\\,)$$$

Lean4

instance partialOrder [PartialOrder α] [PartialOrder β] : PartialOrder (α ⊕ₗ β) :=
  { Lex.preorder with le_antisymm := fun _ _ => antisymm_of (Lex (· ≤ ·) (· ≤ ·)) }

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