iSup_of_empty'

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#iSup_of_empty'

English

If the index type is empty, iSup f equals the supremum of the empty set: iSup f = sSup ∅.

Русский

Если множество индексов пусто, то iSup f равен супремуму пустого множества: iSup f = sSup ∅.

LaTeX

$$$$ \iSup f = \operatorname{sSup}}( \emptyset ) $$$$

Lean4

theorem iSup_of_empty' {α ι} [SupSet α] [IsEmpty ι] (f : ι → α) : iSup f = sSup (∅ : Set α) :=
  congr_arg sSup (range_eq_empty f)

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

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

Разделы

Аффилиация

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