English
Let s ⊆ ι, t ⊆ κ be finite, hst : (s ×ˢ t) ≠ ∅, and f : ι → α, g : κ → β. Then\n\\[ inf' (s ×ˢ t) hst (Prod.map f g) = (inf' s hst.fst f, inf' t hst.snd g). \\]
Русский
Пусть s ⊆ ι, t ⊆ κ конечны и hst ≠ ∅. Тогда\n\\[ \\inf' (s ×ˢ t) hst (Prod.map f g) = (\\inf' s hst.fst f, \\inf' t hst.snd g). \\]
LaTeX
$$$$ \\inf' (s \\times\\! t) hst (\\mathrm{Prod.map}\\, f\\, g) = (\\inf' s hst.fst f, \\inf' t hst.snd g). $$$$
Lean4
/-- See also `Finset.prodMk_inf'_inf'`. -/
-- @[simp] -- TODO: Why does `Prod.map_apply` simplify the LHS?
theorem inf'_prodMap (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) :
inf' (s ×ˢ t) hst (Prod.map f g) = (inf' s hst.fst f, inf' t hst.snd g) :=
(prodMk_inf'_inf' _ _ _ _).symm
