# 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 instDecidablePairwiseToSetOfDecidableEqOfDecidableRel {α : Type u_1} [] {r : ααProp} [] {s : } :
Decidable ((s).Pairwise r)
Equations
• instDecidablePairwiseToSetOfDecidableEqOfDecidableRel = decidable_of_iff' (as, bs, a br a b)
theorem Finset.pairwiseDisjoint_range_singleton {α : Type u_1} :
(Set.range singleton).PairwiseDisjoint id
theorem Set.PairwiseDisjoint.elim_finset {α : Type u_1} {ι : Type u_2} {s : Set ι} {f : ι} (hs : s.PairwiseDisjoint f) {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_1} {ι : Type u_2} [] [] [] {s : } {f : ια} (hs : (s).PairwiseDisjoint f) {g : ιι} (hf : ∀ (a : ι), f (g a) f a) :
(()).PairwiseDisjoint f
theorem Set.PairwiseDisjoint.attach {α : Type u_1} {ι : Type u_2} [] [] {s : } {f : ια} (hs : (s).PairwiseDisjoint f) :
(s.attach).PairwiseDisjoint (f Subtype.val)
theorem Set.PairwiseDisjoint.biUnion_finset {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [] [] {s : Set ι'} {g : ι'} {f : ια} (hs : s.PairwiseDisjoint fun (i' : ι') => (g i').sup f) (hg : is, ((g i)).PairwiseDisjoint f) :
(is, (g i)).PairwiseDisjoint f

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

theorem List.pairwise_of_coe_toFinset_pairwise {α : Type u_1} [] {r : ααProp} {l : List α} (hl : (l.toFinset).Pairwise r) (hn : l.Nodup) :
theorem List.pairwise_iff_coe_toFinset_pairwise {α : Type u_1} [] {r : ααProp} {l : List α} (hn : l.Nodup) (hs : ) :
(l.toFinset).Pairwise r
theorem List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint {α : Type u_5} {ι : Type u_6} [] [] [] {l : List ι} {f : ια} (hl : (l.toFinset).PairwiseDisjoint f) (hn : l.Nodup) :
List.Pairwise (Disjoint on f) l
theorem List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint {α : Type u_5} {ι : Type u_6} [] [] [] {l : List ι} {f : ια} (hn : l.Nodup) :
(l.toFinset).PairwiseDisjoint f List.Pairwise (Disjoint on f) l