toFinset_smul — Mathlib

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 _ _ _

Похожие утверждения