iSup_Iio

Mathlib.Order.SuccPred.CompleteLinearOrder

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

English

If x is a succ-limit, then iSup over Iio x equals x.

Русский

Если x является succ-ограниченным пределом, то верхняя граница по элементам Iio x равна x.

LaTeX

$$$ \\text{IsSuccLimit}(x) \\Rightarrow \\big \\lVert iSup a: a\\in Iio(x) \\lVert = x $$$

Lean4

theorem iSup_Iio (h : IsSuccLimit x) : ⨆ a : Iio x, a.1 = x :=
  h.isSuccPrelimit.iSup_Iio

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

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

Разделы

Аффилиация

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