# Documentation

Mathlib.Data.Finset.Pairwise

# Relations holding pairwise on finite sets #

In this file we prove a few results about the interaction of Set.PairwiseDisjoint and Finset, as well as the interaction of List.Pairwise disjoint and the condition of Disjoint on List.toFinset, in Set form.

instance instDecidablePairwiseToSet {α : Type u_1} [inst : ] {r : ααProp} [inst : ] {s : } :
Equations
theorem Set.PairwiseDisjoint.elim_finset {α : Type u_2} {ι : Type u_1} {s : Set ι} {f : ι} (hs : ) {i : ι} {j : ι} (hi : i s) (hj : j s) (a : α) (hai : a f i) (haj : a f j) :
i = j
theorem Set.PairwiseDisjoint.image_finset_of_le {α : Type u_2} {ι : Type u_1} [inst : ] [inst : ] [inst : ] {s : } {f : ια} (hs : Set.PairwiseDisjoint (s) f) {g : ιι} (hf : ∀ (a : ι), f (g a) f a) :
theorem Set.PairwiseDisjoint.bunionᵢ_finset {α : Type u_3} {ι : Type u_2} {ι' : Type u_1} [inst : ] [inst : ] {s : Set ι'} {g : ι'} {f : ια} (hs : Set.PairwiseDisjoint s fun i' => Finset.sup (g i') f) (hg : ∀ (i : ι'), i sSet.PairwiseDisjoint (↑(g i)) f) :
Set.PairwiseDisjoint (Set.unionᵢ fun i => Set.unionᵢ fun h => ↑(g i)) f

Bind operation for Set.PairwiseDisjoint. In a complete lattice, you can use Set.PairwiseDisjoint.bunionᵢ.

theorem List.pairwise_of_coe_toFinset_pairwise {α : Type u_1} [inst : ] {r : ααProp} {l : List α} (hl : Set.Pairwise (↑()) r) (hn : ) :
theorem List.pairwise_iff_coe_toFinset_pairwise {α : Type u_1} [inst : ] {r : ααProp} {l : List α} (hn : ) (hs : ) :
Set.Pairwise (↑()) r
theorem List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] [inst : ] {l : List ι} {f : ια} (hl : ) (hn : ) :
List.Pairwise (Disjoint on f) l
theorem List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] [inst : ] {l : List ι} {f : ια} (hn : ) :
List.Pairwise (Disjoint on f) l