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} [DecidableEq α] {r : ααProp} [DecidableRel r] {s : Finset α} :
Decidable ((s).Pairwise r)
  • 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 : ιFinset α} (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} [SemilatticeInf α] [OrderBot α] [DecidableEq ι] {s : Finset ι} {f : ια} (hs : (s).PairwiseDisjoint f) {g : ιι} (hf : ∀ (a : ι), f (g a) f a) :
((Finset.image g s)).PairwiseDisjoint f
theorem Set.PairwiseDisjoint.attach {α : Type u_1} {ι : Type u_2} [SemilatticeInf α] [OrderBot α] {s : Finset ι} {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} [Lattice α] [OrderBot α] {s : Set ι'} {g : ι'Finset ι} {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} [DecidableEq α] {r : ααProp} {l : List α} (hl : (l.toFinset).Pairwise r) (hn : l.Nodup) :
theorem List.pairwise_iff_coe_toFinset_pairwise {α : Type u_1} [DecidableEq α] {r : ααProp} {l : List α} (hn : l.Nodup) (hs : Symmetric r) :
(l.toFinset).Pairwise r List.Pairwise r l
theorem List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint {α : Type u_5} {ι : Type u_6} [SemilatticeInf α] [OrderBot α] [DecidableEq ι] {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} [SemilatticeInf α] [OrderBot α] [DecidableEq ι] {l : List ι} {f : ια} (hn : l.Nodup) :
(l.toFinset).PairwiseDisjoint f List.Pairwise (Disjoint on f) l