Theorems · Theorem · combinatorics
Set.Finite.prod
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s.Finite → t.Finite → (s ×ˢ t).Finite- Defined in
- Mathlib.Data.Finite.Prod
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Elemproof · cited by 7,166
- Finiteproof · cited by 3,029
- Set.Finitestatement and proof · cited by 1,814
- SProd.sprodstatement and proof · cited by 1,750
- Set.toFiniteproof · cited by 174
- Set.Finite.to_subtypeproof · cited by 44
Cited by9
Results whose statement or proof uses this declaration.
- Set.Finite.offDiagproof · cited by 4
- HahnSeries.SummableFamily.hasFiniteSupport_smulproof · cited by 3
- Set.infinite_prodproof · cited by 2
- HahnSeries.SummableFamily.smul_support_subset_prodstatement and proof · cited by 2
- HahnSeries.SummableFamily.coeff_smulproof · cited by 2
- Matroid.finite_setOfPred_matroidproof · cited by 2
- Rat.finite_rat_abs_sub_lt_one_div_den_sqproof · cited by 1
- Set.finite_image_fst_and_snd_iffproof · cited by 0
- Set.Finite.toFinset_prodstatement and proof · cited by 0