English
Let α be a ConditionallyCompleteLattice and f : ι → α with range bounded below and ι nonempty. Then the lower interval of the infimum equals the intersection of the lower intervals: Iic(inf_i f_i) = ⋂ i, Iic(f_i).
Русский
Пусть α — условно полночащаяся решетка, f: ι → α с ограниченностью снизу и ι непусто. Тогда Iic(inf_i f(i)) = ⋂ i, Iic(f(i)).
LaTeX
$$$Iic\left(\inf_{i} f(i)\right) = \bigcap_{i} Iic(f(i)).$$$
Lean4
theorem Iic_ciInf [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) : Iic (⨅ i, f i) = ⋂ i, Iic (f i) :=
by
apply Subset.antisymm
· rintro x hx - ⟨i, rfl⟩
exact hx.trans (ciInf_le hf _)
· rintro x hx
apply le_ciInf
simpa using hx