ciSup_false — Mathlib

English

For any function f : False → α in a bottomed conditionally complete lattice, the supremum over the domain is bottom.

Русский

Для любой функции f : False → α внизующем условном полноупорядоченном множестве верхняя грань по области определения равна ⊥.

LaTeX

$$$ iSup f = \bot $$$

Lean4

theorem ciSup_false (f : False → α) : ⨆ i, f i = ⊥ :=
  ciSup_of_empty f

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