English
In a Preorder, the nonempty intersection of all downward closed sets Iic(f(i)) is equivalent to the existence of a global lower bound for the range of f.
Русский
В предрядовой структуре непустое пересечение всех множеств Iic(f(i)) эквивалентно существованию нижней границы для множества {f(i)}.
LaTeX
$$$$ (\\bigcap_i Iic(f(i))).Nonempty \\iff \\exists a, \\forall i, a \\le f(i). $$$$
Lean4
theorem nonempty_iInter_Iic_iff [Preorder α] {f : ι → α} : (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f) :=
by
have : (⋂ (i : ι), Iic (f i)) = lowerBounds (range f) := by ext c; simp [lowerBounds]
simp [this, BddBelow]