subset_sSup_of_not_bddAbove — Mathlib

English

If a subset t of s is not bounded above, then its supremum in s is the default element.

Русский

Если множество t ⊆ s не ограничено сверху, то его супремум в s равен дефолтному элементу.

LaTeX

$$$$ \neg \operatorname{BddAbove}(t) \Rightarrow \operatorname{sSup}(t) = \text{default}. $$$$

Lean4

theorem subset_sSup_of_not_bddAbove [Inhabited s] {t : Set s} (ht : ¬BddAbove t) : sSup t = default := by
  simp [sSup, ht]

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