English
Let s ⊆ β, t ⊆ κ be nonempty finite sets, f: ι → α, g: κ → β. Then\n\\[ (inf' s hs f, inf' t ht g) = inf' (s ×ˢ t) (hs.product ht) (Prod.map f g). \\]
Русский
Пусть s ⊆ β и t ⊆ κ непустые конечные. Тогда\n\\[ \\left( \\inf' s hs f, \\inf' t ht g \\right) = \\inf' (s \\timesˢ t) (hs.product ht) (Prod.map f g). \\]
LaTeX
$$$$ (\\inf' s hs f, \\inf' t ht g) = \\inf' (s \\times\\! t) (hs.product ht) (\\mathrm{Prod.map}\\, f\\, g). $$$$
Lean4
/-- See also `Finset.inf'_prodMap`. -/
theorem prodMk_inf'_inf' (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
(inf' s hs f, inf' t ht g) = inf' (s ×ˢ t) (hs.product ht) (Prod.map f g) :=
prodMk_sup'_sup' (α := αᵒᵈ) (β := βᵒᵈ) hs ht _ _
