iInf_lt_top — Mathlib

English

For a family s: ι → α in a complete lattice α, the infimum of s is strictly less than top if and only if some s(i) is strictly less than top.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem iInf_lt_top : ⨅ i, s i < ⊤ ↔ ∃ i, s i < ⊤ := by simp [lt_top_iff_ne_top]

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