down_iSup — Mathlib

English

If f is a family of lifted elements f(i) ∈ ULift α, then taking the down-value commutes with iSup: the down of the supremum equals the supremum of the downs.

Русский

Пусть f(i) ∈ ULift α; нижняя часть сверху (down) и т. д. коммутируют с iSup: down(⨆i, f(i)) = ⨆i, down(f(i)).

LaTeX

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

Lean4

theorem down_iSup [SupSet α] (f : ι → ULift.{v} α) : (⨆ i, f i).down = ⨆ i, (f i).down :=
  congr_arg sSup <| (preimage_eq_iff_eq_image ULift.up_bijective).mpr <| Eq.symm (range_comp _ _).symm

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