le_iInf_const

Mathlib.Order.CompleteLattice.Basic

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

English

For any fixed a and any nonempty index type ι, a is bounded above by the infimum over all i of a: a ≤ ⨅ _ : ι, a.

Русский

Для произвольного a и непустого ι выполнено: a ≤ ⨅_ι a.

LaTeX

$$$a \\\\le \\\\big\\\\wedge_{- : ι} a$$$

Lean4

theorem le_iInf_const : a ≤ ⨅ _ : ι, a :=
  le_iInf fun _ => le_rfl

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

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

Разделы

Аффилиация

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