Theorems · Definition · combinatorics
Multiset.Sections
{α : Type u_1} → Multiset (Multiset α) → Multiset (Multiset α)The sections of a multiset of multisets s consists of all those multisets
which can be put in bijection with s, so each element is a member of the corresponding multiset.
- Defined in
- Mathlib.Data.Multiset.Sections
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.mapproof · cited by 876
- Multiset.consproof · cited by 313
- Multiset.bindproof · cited by 59
- Multiset.recOnproof · cited by 4
Cited by7
Results whose statement or proof uses this declaration.
- Multiset.sections_consstatement · cited by 4
- Multiset.mem_sectionsstatement and proof · cited by 0
- Multiset.sections_addstatement and proof · cited by 0
- Multiset.sections_zerostatement · cited by 0
- Multiset.card_sectionsstatement and proof · cited by 0
- Multiset.coe_sectionsstatement · cited by 0
- Multiset.prod_map_sumstatement and proof · cited by 0