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 bottom element: iSup f = ⊥.

Русский

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

LaTeX

$$$$ \iSup f = \bot $$$$

Lean4

theorem iSup_of_empty [IsEmpty ι] (f : ι → α) : iSup f = ⊥ :=
  (iSup_of_empty' f).trans sSup_empty

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

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

Разделы

Аффилиация

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