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]