Pairwise relations on a multiset

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

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