mathlib documentation

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.

theorem set.pairwise_disjoint.elim_finset {α : Type u_1} {ι : Type u_2} [decidable_eq α] {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.