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 : DecidableEq α] {r : ααProp} [inst : DecidableRel r] {s : Finset α} :
Equations
theorem Set.PairwiseDisjoint.elim_finset {α : Type u_2} {ι : Type u_1} {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_2} {ι : Type u_1} [inst : DecidableEq ι] [inst : SemilatticeInf α] [inst : OrderBot α] {s : Finset ι} {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 : Lattice α] [inst : 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 (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 : 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} [inst : DecidableEq α] {r : ααProp} {l : List α} (hn : List.Nodup l) (hs : Symmetric r) :
theorem List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst : OrderBot α] [inst : 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_1} {ι : Type u_2} [inst : SemilatticeInf α] [inst : OrderBot α] [inst : DecidableEq ι] {l : List ι} {f : ια} (hn : List.Nodup l) :