ciSup_of_empty

Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

English

If the index set ι is empty, then the supremum of f is the bottom element ⊥.

Русский

Если множество индексов ι пусто, то верхняя грань функции f равна нижнему элементу ⊥.

LaTeX

$$$ \text{IsEmpty}(\iota) \Rightarrow \sup_{i \in \iota} f(i) = \bot $$$

Lean4

@[simp]
theorem ciSup_of_empty [IsEmpty ι] (f : ι → α) : ⨆ i, f i = ⊥ := by rw [iSup_of_empty', csSup_empty]

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

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

Разделы

Аффилиация

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