inf_Ici

Mathlib.Order.Interval.Finset.Basic

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

← MathLib Explorer

English

The infimum of the Ici(a) interval with the identity function is a; i.e., inf id over Ici(a) equals a.

Русский

Наименьшая граница для Ici(a) функции идентичности равна a; то есть inf id over Ici(a) = a.

LaTeX

$$$ (Ici(a)).inf id = a $$$

Lean4

@[simp]
theorem inf_Ici [OrderTop α] (a : α) : (Ici a).inf id = a :=
  le_antisymm (inf_le (f := id) <| mem_Ici.2 <| le_refl a) <| Finset.le_inf fun _ ↦ mem_Ici.1

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

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

Разделы

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

Аффилиация

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