ciInf_le

Mathlib.Order.ConditionallyCompleteLattice.Indexed

URI: https://scilib.ai/kg/mathlib#ciInf_le

← MathLib Explorer

English

If f is bounded below, then iInf f ≤ f(c) for every c.

Русский

Пусть f ограничена снизу; тогда iInf f ≤ f(c) для любого c.

LaTeX

$$BddBelow(range f) → ∀ c, iInf f ≤ f(c)$$

Lean4

/-- The indexed infimum of a function is bounded above by the value taken at one point -/
theorem ciInf_le {f : ι → α} (H : BddBelow (range f)) (c : ι) : iInf f ≤ f c :=
  le_ciSup (α := αᵒᵈ) H c

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

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

Разделы

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

Аффилиация

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