sup_Iic

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.sup_Iic

← MathLib Explorer

English

The supremum of the identity on Iic(a) is a; i.e., (Iic(a)).sup id = a.

Русский

Наивысшая граница функции идентичности на Iic(a) равна a; то есть (Iic(a)).sup id = a.

LaTeX

$$$ (Iic(a)).sup id = a $$$

Lean4

@[simp]
theorem sup_Iic [OrderBot α] (a : α) : (Iic a).sup id = a :=
  le_antisymm (Finset.sup_le fun _ ↦ mem_Iic.1) <| le_sup (f := id) <| mem_Iic.2 <| le_refl a

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

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

Разделы

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

Аффилиация

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