down_iInf — Mathlib

English

If f(i) ∈ ULift α, then the down-value of the iInf equals the iInf of the downs: (⨅ i, f i).down = ⨅ i, (f i).down.

Русский

Пусть f(i) ∈ ULift α; опускание инфимума равно инфимума опусканий: (⨅ i, f i).down = ⨅ i, (f i).down.

LaTeX

$$$\\left(\\bigwedge_{i} f(i)\\right)\\downarrow = \\bigwedge_{i} \\bigl(f(i)\\downarrow\\bigr)$$$

Lean4

theorem down_iInf [InfSet α] (f : ι → ULift.{v} α) : (⨅ i, f i).down = ⨅ i, (f i).down :=
  congr_arg sInf <| (preimage_eq_iff_eq_image ULift.up_bijective).mpr <| Eq.symm (range_comp _ _).symm

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