mathlib documentation


Relations holding pairwise on finite sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [decidable_rel r] {s : finset α} :
theorem set.pairwise_disjoint.elim_finset {α : Type u_1} {ι : Type u_2} {s : set ι} {f : ι finset α} (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 ι] [semilattice_inf α] [order_bot α] {s : finset ι} {f : ι α} (hs : s.pairwise_disjoint f) {g : ι ι} (hf : (a : ι), f (g a) f a) :
theorem set.pairwise_disjoint.bUnion_finset {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [lattice α] [order_bot α] {s : set ι'} {g : ι' finset ι} {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) :