Theorems · Theorem · order theory
Set.Finite.finite_subsets
∀ {α : Type u} {a : Set α}, a.Finite → {b | b ⊆ a}.FiniteThere are finitely many subsets of a given finite set
- Defined in
- Mathlib.Data.Set.Finite.Powerset
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
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
- Finsetproof · cited by 13,712
- SetLike.coeproof · cited by 8,199
- Set.ofPredstatement and proof · cited by 6,101
- Set.imageproof · cited by 5,609
- Set.preimageproof · cited by 4,946
- Set.extproof · cited by 2,266
- Set.Finitestatement and proof · cited by 1,814
- Finset.mapproof · cited by 747
- Set.image_congrproof · cited by 533
- Set.Finite.toFinsetproof · cited by 351
- Set.Finite.subsetproof · cited by 285
Cited by5
Results whose statement or proof uses this declaration.
- Set.Finite.powersetproof · cited by 5
- Matroid.finite_setOfPred_matroidproof · cited by 2
- ProbabilityTheory.map_ncard_setBernoulli_real_singletonproof · cited by 2
- Matroid.finite_setOfPred_isRestrictionproof · cited by 1
- MeasureTheory.LevyProkhorov.continuous_ofMeasure_probabilityMeasureproof · cited by 1