iInf_eq_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem iInf_eq_top : iInf s = ⊤ ↔ ∀ i, s i = ⊤ :=
  sInf_eq_top.trans forall_mem_range

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