Extensions to Set

The intention is to upstream these to mathlib or to find and use similar existing theorems in mathlib.

theorem Set.PairwiseDisjoint_iff {α : Type u_1} {β : Type u_2} {S : Set α} {f : α → Set β} : S.PairwiseDisjoint f ↔ ∀ {x : β} {a b : α}, a ∈ S → b ∈ S → x ∈ f a → x ∈ f b → a = b