Iic_iInf — Mathlib

English

In a complete lattice, the set of elements below the infimum ⨅ i f(i) equals the intersection of the sets below each f(i).

Русский

В полной решётке множество элементов, не превосходящих наибольшего общего снизу ⨅ i f(i), равно пересечению множеств, не превосходящих каждого f(i).

LaTeX

$$$$ \\{ x \\in \\alpha \\mid x \\le \\bigwedge_i f(i) \\} = \\bigcap_i \\{ x \\in \\alpha \\mid x \\le f(i) \\} $$$$

Lean4

theorem Iic_iInf (f : ι → α) : Iic (⨅ i, f i) = ⋂ i, Iic (f i) :=
  ext fun _ => by simp only [mem_Iic, le_iInf_iff, mem_iInter]

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