ciInf_const

Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

English

The infimum of a constant function over a nonempty index set is that constant.

Русский

infimum константной функции над непустым индексным множеством равен самой константе.

LaTeX

$$iInf (fun _ : ι => a) = a$$

Lean4

@[simp]
theorem ciInf_const [Nonempty ι] {a : α} : ⨅ _ : ι, a = a :=
  ciSup_const (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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