English
Let s ⊆ β and t ⊆ κ be nonempty finite sets, f: ι → α, g: κ → β. Then\n\\[ { fst := s.sup' hs f, snd := t.sup' ht g } = (Finset.instSProd.sprod s t).sup' (Prod.map f g). $$
Русский
Пусть s ⊆ β и t ⊆ κ непустые конечные. Тогда существование пары равняется\n\\[ \\{ fst := s.sup' hs f, snd := t.sup' ht g \\} = (s ×ˢ t).sup' (Prod.map f g). $$
LaTeX
$$$$ (s \\sup' hs f, t \\sup' ht g) = (s \\times\\! t)^{\\sup'} (hs.product ht) (\\mathrm{Prod.map}\\, f\\, g). $$$$
Lean4
/-- See also `Finset.prodMk_sup'_sup'`. -/
-- @[simp] -- TODO: Why does `Prod.map_apply` simplify the LHS?
theorem sup'_prodMap (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) :
sup' (s ×ˢ t) hst (Prod.map f g) = (sup' s hst.fst f, sup' t hst.snd g) :=
(prodMk_sup'_sup' _ _ _ _).symm
