iSup_of_empty

Mathlib.SetTheory.Cardinal.Basic

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

← MathLib Explorer

English

If the index type ι is empty, then iSup f = 0 for any f : ι → Cardinal.

Русский

Если множество индексов ι пусто, то iSup f = 0 для любого f : ι → Cardinal.

LaTeX

$$$IsEmpty\, ι \Rightarrow iSup f = 0$$$

Lean4

/-- A variant of `ciSup_of_empty` but with `0` on the RHS for convenience -/
protected theorem iSup_of_empty {ι} (f : ι → Cardinal) [IsEmpty ι] : iSup f = 0 :=
  ciSup_of_empty f

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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