sup'_Iic

Mathlib.Order.Interval.Finset.Basic

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

← MathLib Explorer

English

The supremum (with id) over Iic(a) equals a; i.e., the maximum of Iic(a) under the identity function is a.

Русский

Наименьшее верхнее (sup') по Iic(a) с именем id равно a; то есть максимум Iic(a) равен a.

LaTeX

$$$ (Iic(a)).sup' \text{ id} = a $$$

Lean4

theorem sup'_Iic (a : α) : (Iic a).sup' nonempty_Iic id = a :=
  le_antisymm (sup'_le _ _ fun _ ↦ mem_Iic.1) <| le_sup' (f := id) <| mem_Iic.2 <| le_refl a

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

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

Разделы

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

Аффилиация

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