instLinearOrderLex — Mathlib

English

Let α be a type equipped with a linear order. Then Lex(NonemptyInterval α) carries a natural linear order; in particular, Lex(NonemptyInterval α) is linearly ordered.

Русский

Пусть α — множество с линейным порядком. Тогда Lex(NonemptyInterval α) наделено естественным линейным порядком; то есть оно линейно упорядовано.

LaTeX

$$$\forall \alpha\, (\mathsf{LinearOrder}(\alpha)) \Rightarrow \mathsf{LinearOrder}(\mathrm{Lex}(\mathrm{NonemptyInterval}(\alpha))).$$$

Lean4

instance [LinearOrder α] : LinearOrder (Lex (NonemptyInterval α)) :=
  fast_instance%{
      LinearOrder.lift' (fun x : Lex (NonemptyInterval α) => toLex (ofLex x).toDualProd) <|
        toLex.injective.comp <|
          toDualProd_injective.comp ofLex.injective with
      toDecidableEq := inferInstance
      toDecidableLT := inferInstance
      toDecidableLE := inferInstance }

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