iSup_const

Mathlib.Order.CompleteLattice.Basic

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

English

If ι is nonempty, the supremum of a constant a over ι equals a: ⨆ i, a = a.

Русский

Если ι непусто, то ⨆ i a = a.

LaTeX

$$$\\\\iSup i\, a = a$$$

Lean4

theorem iSup_const [Nonempty ι] : ⨆ _ : ι, a = a := by rw [iSup, range_const, sSup_singleton]

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

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

Разделы

Аффилиация

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