bot_lt_iSup — Mathlib

English

For a function s: ι → α in a complete lattice α, the bottom element is strictly less than the supremum of the s(i) if and only if there exists some i with ⊥ < s(i).

Русский

Для функции s: ι → α в полной решётке α нижняя граница ⊥ строго меньше супремума по s(i) тогда и только тогда, когда существует i с ⊥ < s(i).

LaTeX

$$$$\bot < \bigvee_{i : ι} s(i) \;\Longleftrightarrow\; \exists i, \bot < s(i).$$$$

Lean4

@[simp]
theorem bot_lt_iSup : ⊥ < ⨆ i, s i ↔ ∃ i, ⊥ < s i := by simp [bot_lt_iff_ne_bot]

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