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_reducible]

instance instDecidablePairwiseCoeFinsetOfDecidableEqOfDecidableRel {α : Type u_1} [DecidableEq α] {r : α → α → Prop} [DecidableRel r] {s : Finset α} : Decidable ((↑s).Pairwise r)

Equations

• instDecidablePairwiseCoeFinsetOfDecidableEqOfDecidableRel = decidable_of_iff' (∀ a ∈ s, ∀ b ∈ s, a ≠ b → r 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} [PartialOrder α] [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} [PartialOrder α] [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 : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f) : (⋃ i ∈ s, ↑(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) : Pairwise r l

theorem List.pairwise_iff_coe_toFinset_pairwise {α : Type u_1} [DecidableEq α] {r : α → α → Prop} {l : List α} [Std.Symm r] (hn : l.Nodup) : (↑l.toFinset).Pairwise r ↔ Pairwise r l

theorem List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint {α : Type u_4} {ι : Type u_5} [PartialOrder α] [OrderBot α] [DecidableEq ι] {l : List ι} {f : ι → α} (hl : (↑l.toFinset).PairwiseDisjoint f) (hn : l.Nodup) : Pairwise (Function.onFun _root_.Disjoint f) l

theorem List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint {α : Type u_4} {ι : Type u_5} [PartialOrder α] [OrderBot α] [DecidableEq ι] {l : List ι} {f : ι → α} (hn : l.Nodup) : (↑l.toFinset).PairwiseDisjoint f ↔ Pairwise (Function.onFun _root_.Disjoint f) l