Iic_ciInf — Mathlib

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

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