isLUB_sup'

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.isLUB_sup'

← MathLib Explorer

English

sup' acts as the least upper bound of the set {f(x) : x ∈ s} in the appropriate order.

Русский

sup' является наименьшей верхней границей множества значений {f(x) : x ∈ s}.

LaTeX

$$$IsLUB\, s\; (sup' s hs\; id)$$$

Lean4

theorem isLUB_sup' {s : Finset α} (hs : s.Nonempty) : IsLUB s (sup' s hs id) :=
  ⟨fun x h => id_eq x ▸ le_sup' id h, fun _ h => Finset.sup'_le hs id h⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru