instPreorderLex — Mathlib

English

Definition: If α has a preorder, then the type Lex(NonemptyInterval α) is equipped with a preorder defined by x ≤ y iff toLex x ≤ toLex y.

Русский

Определение: если у α есть предорядок, то у Lex(NonemptyInterval α) есть предраспорядок, задаваемый x ≤ y ⇔ toLex(x) ≤ toLex(y).

LaTeX

$$$ x \le y \;\text{на} \mathrm{Lex}(\mathrm{NonemptyInterval}(\alpha)) \iff toLex(x) \le toLex(y) $$$

Lean4

instance [Preorder α] : Preorder (Lex (NonemptyInterval α)) :=
  fast_instance%Preorder.lift fun x => toLex (ofLex x).toDualProd

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