csInf_upperBounds_eq_csSup

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#csInf_upperBounds_eq_csSup

← MathLib Explorer

English

If IsLUB s a and s is nonempty, then sSup s = a.

Русский

Если IsLUB s a и s непусто, то sSup s = a.

LaTeX

$$$IsLUB(s, a) \land s \neq \varnothing \rightarrow \mathrm{sSup}(s) = a$$$

Lean4

theorem csInf_upperBounds_eq_csSup {s : Set α} (h : BddAbove s) (hs : s.Nonempty) : sInf (upperBounds s) = sSup s :=
  (isGLB_csInf h <| hs.mono fun _ hx _ hy => hy hx).unique (isLUB_csSup hs h).isGLB

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

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

Разделы

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

Аффилиация

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