Theorems · Definition · combinatorics
Multiset.Pairwise
{α : Type u_1} → (α → α → Prop) → Multiset α → PropPairwise r m states that there exists a list of the elements s.t. r holds pairwise on this
list.
- Defined in
- Mathlib.Data.Multiset.Defs
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
Cited by9
Results whose statement or proof uses this declaration.
- Multiset.pairwise_coe_iff_pairwisestatement and proof · cited by 2
- Multiset.Nodup.pairwisestatement · cited by 1
- Multiset.support_sum_eqstatement and proof · cited by 1
- Multiset.nodup_iff_pairwisestatement · cited by 0
- Multiset.pairwise_zerostatement · cited by 0
- Finset.support_sum_eqproof · cited by 0
- Multiset.nodup_bindstatement and proof · cited by 0
- Multiset.Pairwise.forallstatement and proof · cited by 0
- Multiset.pairwise_coe_iffstatement · cited by 0