sInf_upperBounds_eq_csSup

Mathlib.Order.CompleteLattice.Basic

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

English

For any set s in α, the infimum of the upper bounds of s equals the supremum of s.

Русский

Для множества s в α инфинуум верхних границ s равен супремуму самого множества s.

LaTeX

$$$\\\\forall s:\\\\ Set α, \\\\ sInf (upperBounds s) = sSup s$$$

Lean4

theorem sInf_upperBounds_eq_csSup (s : Set α) : sInf (upperBounds s) = sSup s :=
  (isGLB_sInf _).unique (isLUB_sSup _).isGLB

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

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

Разделы

Аффилиация

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