instPartialOrderLex — Mathlib

English

If α is a PartialOrder, then Lex(NonemptyInterval α) is equipped with a PartialOrder defined by x ≤ y iff toLex x ≤ toLex y.

Русский

Если α частично упорядочено, то Lex(NonemptyInterval α) оснащён частичным порядком, определяемым x ≤ y ⇔ toLex x ≤ toLex y.

LaTeX

$$$ x \le y \iff toLex(x) \le toLex(y) \quad(\text{on } \mathrm{Lex}(\mathrm{NonemptyInterval}(\alpha)))$$$

Lean4

instance [PartialOrder α] : PartialOrder (Lex (NonemptyInterval α)) :=
  fast_instance%PartialOrder.lift (fun x => toLex (ofLex x).toDualProd) <|
      toLex.injective.comp <| toDualProd_injective.comp ofLex.injective

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