le_iInf

Mathlib.Order.CompleteLattice.Basic

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

English

If a ≤ f(i) for all i, then a ≤ iInf f.

Русский

Если $a \\le f(i)$ для всех $i$, то $a \\le \\inf_i f(i)$.

LaTeX

$$$$a \\le f(i) \\; \\forall i \\Rightarrow \\; a \\le \\iInf_i f(i).$$$$

Lean4

theorem le_iInf (h : ∀ i, a ≤ f i) : a ≤ iInf f :=
  le_sInf fun _ ⟨i, Eq⟩ => Eq ▸ h i

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

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

Разделы

Аффилиация

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