instPreorder — Mathlib

English

If α,β,γ are Preorder, then NonemptyInterval α is a Preorder, induced by toDualProd.

Русский

Если α, β, γ — предпорядки, то NonemptyInterval α имеет порядок, индуцированный через toDualProd.

LaTeX

$$$\text{Preorder}(\mathrm{NonemptyInterval}\;\alpha)$, определённый через $s \le t$ iff $t.fst \le s.fst$ и $s.snd \le t.snd$.$$

Lean4

instance : Preorder (NonemptyInterval α) :=
  Preorder.lift toDualProd

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