sSup_Iio

Mathlib.Order.SuccPred.CompleteLinearOrder

URI: https://scilib.ai/kg/mathlib#Order.IsSuccLimit.sSup_Iio

English

If x is a succ-limit, then sSup(Iio x) = x.

Русский

Если x является succ-ограниченным пределом, то наибольшая верхняя грань множества {y: y < x} равна x.

LaTeX

$$$ sSup(Iio x) = x $$$

Lean4

theorem sSup_Iio (h : IsSuccLimit x) : sSup (Iio x) = x :=
  h.isSuccPrelimit.sSup_Iio

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

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

Разделы

Аффилиация

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