English
Let α and β be SupSet spaces and s ⊆ α, t ⊆ β be nonempty. Then the supremum of the product set s ×ˢ t is the pair of sups: sSup (s ×ˢ t) = (sSup s, sSup t).
Русский
Пусть α и β — надмножественные пространства; s и t непустые. Тогда верхняя граница произведения равна паре верхних границ по координатам: sSup (s × t) = (sSup s, sSup t).
LaTeX
$$$ sSup (s \timesˢ t) = (sSup s, sSup t) $$$
Lean4
theorem sSup_prod [SupSet α] [SupSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) :
sSup (s ×ˢ t) = (sSup s, sSup t) :=
congr_arg₂ Prod.mk (congr_arg sSup <| fst_image_prod _ ht)
(congr_arg sSup <| snd_image_prod hs _)
-- See note [reducible non-instances]
