feat(data/fintype/basic): fintype.to_finset_prod (#16459)

leanprover-community · Sep 11, 2022 · c8c740d · c8c740d
1 parent 5e78882
commit c8c740d
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
@@ -675,6 +675,10 @@ theorem to_finset_compl [decidable_eq α] [fintype α] (s : set α) [fintype s]
   (sᶜ).to_finset = s.to_finsetᶜ :=
 by { ext, simp }
 
+lemma to_finset_prod (s : set α) (t : set β) [fintype s] [fintype t] [fintype (s ×ˢ t)] :
+  (s ×ˢ t).to_finset = s.to_finset ×ˢ t.to_finset :=
+by { ext, simp }
+
 /- TODO Without the coercion arrow (`↥`) there is an elaboration bug;
 it essentially infers `fintype.{v} (set.univ.{u} : set α)` with `v` and `u` distinct.
 Reported in leanprover-community/lean#672 -/