English
Let s ⊆ β, t ⊆ κ be nonempty finite sets, f: ι → α, g: κ → β. Then\n\\[ (\\sup' s hs f, \\sup' t ht g) = \\sup' (s ×ˢ t) (hs.product ht) (Prod.map f g). \\]
Русский
Пусть s ⊆ β, t ⊆ κ непустые конечные, f: ι → α, g: κ → β. Тогда\n\\[ (\\sup' s hs f, \\sup' t ht g) = \\sup' (s \\timesˢ t) (hs.product ht) (Prod.map f g). \\]
LaTeX
$$$$ (\\sup' s hs f, \\sup' t ht g) = \\sup' (s \\times\\! t) (hs \\cdot ht) (\\mathrm{Prod.map}\\, f\\, g). $$$$
Lean4
/-- See also `Finset.sup'_prodMap`. -/
theorem prodMk_sup'_sup' (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
(sup' s hs f, sup' t ht g) = sup' (s ×ˢ t) (hs.product ht) (Prod.map f g) :=
eq_of_forall_ge_iff fun i ↦ by
obtain ⟨a, ha⟩ := hs
obtain ⟨b, hb⟩ := ht
simp only [Prod.map, sup'_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]
exact ⟨by simp_all, fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩⟩
