instPartialOrder — Mathlib

English

NonemptyInterval α carries a natural partial order: s ≤ t iff the underlying interval Icc(s.fst, s.snd) is contained in Icc(t.fst, t.snd).

Русский

NonemptyInterval α имеет естественный частичный порядок: s ≤ t тогда и только если Icc(s.fst, s.snd) ⊆ Icc(t.fst, t.snd).

LaTeX

$$$ s \le t \iff \mathrm{Icc}(s.fst,s.snd) \subseteq \mathrm{Icc}(t.fst,t.snd) $$$

Lean4

instance : PartialOrder (NonemptyInterval α) :=
  PartialOrder.lift _ toDualProd_injective

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