Theorems · Theorem · combinatorics
Multiset.card_le_card
∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → s.card ≤ t.card- Defined in
- Mathlib.Data.Multiset.Defs
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement and proof · cited by 2,627
- Multiset.cardstatement · cited by 375
- Multiset.leInductionOnproof · cited by 12
Cited by11
Results whose statement or proof uses this declaration.
- Finset.card_le_cardproof · cited by 118
- Multiset.toFinset_card_leproof · cited by 10
- Multiset.map_lt_mapproof · cited by 3
- card_rootsOfUnityproof · cited by 2
- Polynomial.roots_expand_pow_map_iterateFrobenius_leproof · cited by 2
- Multiset.card_monoproof · cited by 1
- MvPolynomial.totalDegree_le_degrees_cardproof · cited by 1
- Polynomial.card_le_degree_of_subset_rootsproof · cited by 1
- Multiset.card_erase_leproof · cited by 1
- Polynomial.card_roots_le_mapproof · cited by 1
- Multiset.card_filter_le_iffproof · cited by 1