Pairwise relations on a multiset

This file provides basic results about Multiset.Pairwise (definitions are in Mathlib.Data.Multiset.Defs).

theorem Multiset.Pairwise.forall {α : Type u_1} {r : α → α → Prop} {s : Multiset α} (H : Symmetric r) (hs : Pairwise r s) ⦃a : α⦄ : a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≠ b → r a b