English
If α and β are complete lattices and f,i ↦ f i, g,i ↦ g i are functions from ι to α and β respectively, then the supremum over i of the pair (f i, g i) equals the pair of suprema, i.e. ⨆ i, (f i, g i) = (⨆ i, f i, ⨆ i, g i).
Русский
Если α и β — полные решетки и заданы функции f i ∈ α и g i ∈ β, то верхняя граница по индексу i для пары (f i, g i) равна паре верхних границ по каждому компоненту: ⨆ i, (f i, g i) = (⨆ i, f i, ⨆ i, g i).
LaTeX
$$$ ⨆ i, (f i, g i) = (⨆ i, f i, ⨆ i, g i) $$$
Lean4
theorem iSup_mk [SupSet α] [SupSet β] (f : ι → α) (g : ι → β) : ⨆ i, (f i, g i) = (⨆ i, f i, ⨆ i, g i) :=
congr_arg₂ Prod.mk (fst_iSup _) (snd_iSup _)
