ciSup_const

Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem ciSup_const [hι : Nonempty ι] {a : α} : ⨆ _ : ι, a = a := by rw [iSup, range_const, csSup_singleton]

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

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

Разделы

Аффилиация

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