toFinset_prod — Mathlib

English

For finite sets s and t, the toFinset of the product s × t equals the product of toFinsets.

Русский

Для конечных множеств S и T множество toFinset(S × T) совпадает с произведением toFinset(S) и toFinset(T).

LaTeX

$$$ hs.toFinset \times ht.toFinset = (hs.prod ht).toFinset $$$

Lean4

theorem toFinset_prod {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) :
    hs.toFinset ×ˢ ht.toFinset = (hs.prod ht).toFinset :=
  Finset.ext <| by simp

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