English
For sets with scalar action, the Finset of the product equals the product of Finsets: (s • t).toFinset = s.toFinset • t.toFinset.
Русский
Для множеств с действием скаляра отображение в Finset сохраняет произведение: (s • t).toFinset = s.toFinset • t.toFinset.
LaTeX
$$$\\bigl(s \\cdot t\\bigr)^{\\!\\text{toFinset}} = s^{\\!\\text{toFinset}} \\cdot t^{\\!\\text{toFinset}}$$$
Lean4
@[to_additive (attr := simp)]
theorem toFinset_smul (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype ↑(s • t)] :
(s • t).toFinset = s.toFinset • t.toFinset :=
toFinset_image2 _ _ _