instPartialOrder — Mathlib

English

The lexicographic order on α × β forms a partial order when α and β are partially ordered.

Русский

Лексикографический порядок на α × β образует частичный порядок, если α и β частично упорядочены.

LaTeX

$$$$ \text{instPartialOrder}(\alpha,\beta) : \text{PartialOrder}(\mathrm{Lex}(\alpha,\beta)). $$$$

Lean4

/-- Dictionary / lexicographic partial order for pairs. -/
instance instPartialOrder (α β : Type*) [PartialOrder α] [PartialOrder β] : PartialOrder (α ×ₗ β) where
  le_antisymm _ _ := antisymm_of (Prod.Lex _ _)

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