Theorems · Theorem · combinatorics
Multiset.nodup_powerset
∀ {α : Type u_1} {s : Multiset α}, s.powerset.Nodup ↔ s.Nodup- Defined in
- Mathlib.Data.Multiset.Powerset
- Cited by
- 3 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.
Cites11
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.ofListproof · cited by 290
- Multiset.Nodupstatement and proof · cited by 148
- Multiset.powersetstatement and proof · cited by 27
- Multiset.nodup_of_leproof · cited by 10
- Multiset.powerset_coe'proof · cited by 9
- List.mem_sublists'proof · cited by 5
- Multiset.Nodup.of_mapproof · cited by 4
- List.Nodup.map_onproof · cited by 4
- List.nodup_sublists'proof · cited by 3
- Multiset.map_single_le_powersetproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- Multiset.Nodup.powersetproof · cited by 0
- Multiset.Nodup.powersetCardproof · cited by 0
- Multiset.Nodup.ofPowersetproof · cited by 0