iSup_eq_bot — Mathlib

English

Let f : ι → α be a family of elements in a complete lattice α. Then the supremum of f equals ⊥ if and only if every f(i) equals ⊥.

Русский

Пусть f : ι → α — семейство элементов полной решётки α. Тогда ⨆ i, f(i) = ⊥ тогда и только тогда, когда ∀ i, f(i) = ⊥.

LaTeX

$$$$\bigvee_{i : ι} f(i) = \bot \quad\Longleftrightarrow\quad \forall i,\; f(i) = \bot.$$$$

Lean4

@[simp]
theorem iSup_eq_bot : iSup s = ⊥ ↔ ∀ i, s i = ⊥ :=
  sSup_eq_bot.trans forall_mem_range

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