mathlibdocumentation

data.finset.pairwise

Relations holding pairwise on finite sets #

In this file we prove a few results about the interaction of set.pairwise_disjoint and finset, as well as the interaction of list.pairwise disjoint and the condition of disjoint on list.to_finset, in set form.

@[protected, instance]
def pairwise.decidable {α : Type u_1} [decidable_eq α] {r : α → α → Prop} {s : finset α} :
Equations
theorem set.pairwise_disjoint.elim_finset {α : Type u_1} {ι : Type u_2} [decidable_eq α] {s : set ι} {f : ι → } (hs : s.pairwise_disjoint f) {i j : ι} (hi : i s) (hj : j s) (a : α) (hai : a f i) (haj : a f j) :
i = j
theorem set.pairwise_disjoint.image_finset_of_le {α : Type u_1} {ι : Type u_2} [decidable_eq ι] [order_bot α] {s : finset ι} {f : ι → α} (hs : s.pairwise_disjoint f) {g : ι → ι} (hf : ∀ (a : ι), f (g a) f a) :
f
theorem set.pairwise_disjoint.bUnion_finset {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [lattice α] [order_bot α] {s : set ι'} {g : ι' → } {f : ι → α} (hs : s.pairwise_disjoint (λ (i' : ι'), (g i').sup f)) (hg : ∀ (i : ι'), i s(g i).pairwise_disjoint f) :
(⋃ (i : ι') (H : i s), (g i)).pairwise_disjoint f

Bind operation for set.pairwise_disjoint. In a complete lattice, you can use set.pairwise_disjoint.bUnion.

theorem list.pairwise_of_coe_to_finset_pairwise {α : Type u_1} [decidable_eq α] {r : α → α → Prop} {l : list α} (hl : (l.to_finset).pairwise r) (hn : l.nodup) :
theorem list.pairwise_iff_coe_to_finset_pairwise {α : Type u_1} [decidable_eq α] {r : α → α → Prop} {l : list α} (hn : l.nodup) (hs : symmetric r) :
theorem list.pairwise_disjoint_of_coe_to_finset_pairwise_disjoint {α : Type u_1} {ι : Type u_2} [order_bot α] [decidable_eq ι] {l : list ι} {f : ι → α} (hl : (l.to_finset).pairwise_disjoint f) (hn : l.nodup) :
l
theorem list.pairwise_disjoint_iff_coe_to_finset_pairwise_disjoint {α : Type u_1} {ι : Type u_2} [order_bot α] [decidable_eq ι] {l : list ι} {f : ι → α} (hn : l.nodup) :
l