Theorems · Theorem · general algebraic systems
Multiset.mem_sup_map_support_iff
∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : Zero M] {s : Multiset (ι →₀ M)} {x : ι},
x ∈ (Multiset.map Finsupp.support s).sup ↔ ∃ f ∈ s, x ∈ f.support- Defined in
- Mathlib.Data.Finsupp.BigOperators
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Finsuppstatement and proof · cited by 5,255
- Multisetstatement and proof · cited by 2,627
- Multiset.mapstatement · cited by 876
- Finsupp.supportstatement and proof · cited by 828
- Multiset.ofListproof · cited by 290
- Multiset.supstatement · cited by 20
- List.mem_foldr_sup_support_iffproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Finset.mem_sup_support_iffproof · cited by 0