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} [DecidableEq α] {r : ααProp} [DecidableRel r] {s : Finset α} :
Equations
theorem Set.PairwiseDisjoint.elim_finset {α : Type u_1} {ι : Type u_2} {s : Set ι} {f : ιFinset α} (hs : Set.PairwiseDisjoint s 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 : Set.PairwiseDisjoint (s) f) {g : ιι} (hf : ∀ (a : ι), f (g a) f a) :
theorem Set.PairwiseDisjoint.attach {α : Type u_1} {ι : Type u_2} [SemilatticeInf α] [OrderBot α] {s : Finset ι} {f : ια} (hs : Set.PairwiseDisjoint (s) f) :
Set.PairwiseDisjoint (↑(Finset.attach s)) (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 : Set.PairwiseDisjoint s fun i' => Finset.sup (g i') f) (hg : ∀ (i : ι'), i sSet.PairwiseDisjoint (↑(g i)) f) :
Set.PairwiseDisjoint (⋃ (i : ι') (_ : i s), ↑(g i)) 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 : Set.Pairwise (↑(List.toFinset l)) r) (hn : List.Nodup l) :
theorem List.pairwise_iff_coe_toFinset_pairwise {α : Type u_1} [DecidableEq α] {r : ααProp} {l : List α} (hn : List.Nodup l) (hs : Symmetric r) :
theorem List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint {α : Type u_5} {ι : Type u_6} [SemilatticeInf α] [OrderBot α] [DecidableEq ι] {l : List ι} {f : ια} (hl : Set.PairwiseDisjoint (↑(List.toFinset l)) f) (hn : List.Nodup l) :
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 : List.Nodup l) :