instOrderTop — Mathlib

English

If α is a bounded order, NonemptyInterval α has a top element, namely the interval [⊥, ⊤], and every interval is below it.

Русский

Если упорядоченность α ограничена сверху и снизу, то у NonemptyInterval α есть верхний элемент, равный интервалу [⊥, ⊤], и каждый интервал лежит ниже него.

LaTeX

$$$\text{top}_{\mathrm{NonemptyInterval}(\alpha)} = [\bot, \top], \quad (\forall s\in \mathrm{NonemptyInterval}(\alpha),\; s \le \top)$$$

Lean4

instance : OrderTop (NonemptyInterval α) where
  top := ⟨⟨⊥, ⊤⟩, bot_le⟩
  le_top _ := ⟨bot_le, le_top⟩

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