Unions of finite sets

This file defines the union of a family t : α → Finset β of finsets bounded by a finset s : Finset α.

Main declarations

• Finset.disjUnion: Given a hypothesis h which states that finsets s and t are disjoint, s.disjUnion t h is the set such that a ∈ disjUnion s t h iff a ∈ s or a ∈ t; this does not require decidable equality on the type α.
• Finset.biUnion: Finite unions of finsets; given an indexing function f : α → Finset β and an s : Finset α, s.biUnion f is the union of all finsets of the form f a for a ∈ s.

TODO

Remove Finset.biUnion in favour of Finset.sup.

def Finset.disjiUnion {α : Type u_1} {β : Type u_2} (s : Finset α) (t : α → Finset β) (hf : (↑s).PairwiseDisjoint t) : Finset β

disjiUnion s f h is the set such that a ∈ disjiUnion s f iff a ∈ f i for some i ∈ s. It is the same as s.biUnion f, but it does not require decidable equality on the type. The hypothesis ensures that the sets are disjoint.

Equations

• s.disjiUnion t hf = { val := s.val.bind (Finset.val ∘ t), nodup := ⋯ }

@[simp]

theorem Finset.disjiUnion_val {α : Type u_1} {β : Type u_2} (s : Finset α) (t : α → Finset β) (h : (↑s).PairwiseDisjoint t) : (s.disjiUnion t h).val = s.val.bind fun (a : α) => (t a).val

@[simp]

theorem Finset.disjiUnion_empty {α : Type u_1} {β : Type u_2} (t : α → Finset β) : ∅.disjiUnion t ⋯ = ∅

@[simp]

theorem Finset.mem_disjiUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} {b : β} {h : (↑s).PairwiseDisjoint t} : b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a

@[simp]

theorem Finset.coe_disjiUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} {h : (↑s).PairwiseDisjoint t} : ↑(s.disjiUnion t h) = ⋃ x ∈ ↑s, ↑(t x)

@[simp]

theorem Finset.disjiUnion_cons {α : Type u_1} {β : Type u_2} (a : α) (s : Finset α) (ha : a ∉ s) (f : α → Finset β) (H : (↑(cons a s ha)).PairwiseDisjoint f) : (cons a s ha).disjiUnion f H = (f a).disjUnion (s.disjiUnion f ⋯) ⋯

@[simp]

theorem Finset.singleton_disjiUnion {α : Type u_1} {β : Type u_2} {t : α → Finset β} (a : α) {h : (↑{a}).PairwiseDisjoint t} : {a}.disjiUnion t h = t a

theorem Finset.disjiUnion_disjiUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Finset α) (f : α → Finset β) (g : β → Finset γ) (h1 : (↑s).PairwiseDisjoint f) (h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g) : (s.disjiUnion f h1).disjiUnion g h2 = s.attach.disjiUnion (fun (a : ↥s) => (f ↑a).disjiUnion g ⋯) ⋯

theorem Finset.sUnion_disjiUnion {α : Type u_1} {β : Type u_2} {f : α → Finset (Set β)} (I : Finset α) (hf : (↑I).PairwiseDisjoint f) : ⋃₀ ↑(I.disjiUnion f hf) = ⋃ a ∈ I, ⋃₀ ↑(f a)

@[simp]

theorem Finset.disjiUnion_filter_eq {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : Finset β) (f : α → β) : t.disjiUnion (fun (a : β) => {x ∈ s | f x = a}) ⋯ = {c ∈ s | f c ∈ t}

theorem Finset.disjiUnion_filter_eq_of_maps_to {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} (h : ∀ x ∈ s, f x ∈ t) : t.disjiUnion (fun (a : β) => {x ∈ s | f x = a}) ⋯ = s

theorem Finset.map_disjiUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α ↪ β} {s : Finset α} {t : β → Finset γ} {h : (↑(map f s)).PairwiseDisjoint t} : (map f s).disjiUnion t h = s.disjiUnion (fun (a : α) => t (f a)) ⋯

theorem Finset.disjiUnion_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : α → Finset β} {f : β ↪ γ} {h : (↑s).PairwiseDisjoint t} : map f (s.disjiUnion t h) = s.disjiUnion (fun (a : α) => map f (t a)) ⋯

@[simp]

theorem Finset.disjiUnion_singleton_eq_self {α : Type u_1} (s : Finset α) : s.disjiUnion singleton ⋯ = s

theorem Finset.fold_disjiUnion {α : Type u_1} {β : Type u_2} {f : α → β} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {ι : Type u_4} {s : Finset ι} {t : ι → Finset α} {b : ι → β} {b₀ : β} (h : (↑s).PairwiseDisjoint t) : fold op (fold op b₀ b s) f (s.disjiUnion t h) = fold op b₀ (fun (i : ι) => fold op (b i) f (t i)) s

theorem Finset.pairwiseDisjoint_filter {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → Finset β} (h : (↑s).PairwiseDisjoint f) (p : β → Prop) [DecidablePred p] : (↑s).PairwiseDisjoint fun (a : α) => filter p (f a)

theorem Finset.filter_disjiUnion {α : Type u_1} {β : Type u_2} (s : Finset α) (f : α → Finset β) (h : (↑s).PairwiseDisjoint f) (p : β → Prop) [DecidablePred p] : filter p (s.disjiUnion f h) = s.disjiUnion (fun (a : α) => filter p (f a)) ⋯

theorem Finset.disjiUnion_singleton {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} (hf : Function.Injective f) : s.disjiUnion (fun (a : α) => {f a}) ⋯ = map { toFun := f, inj' := hf } s

theorem Finset.disjoint_disjiUnion_left {α : Type u_1} {β : Type u_2} (s : Finset α) (f : α → Finset β) (hf : (↑s).PairwiseDisjoint f) (t : Finset β) : Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t

theorem Finset.disjoint_disjiUnion_right {α : Type u_1} {β : Type u_2} (s : Finset β) (t : Finset α) (f : α → Finset β) (hf : (↑t).PairwiseDisjoint f) : Disjoint s (t.disjiUnion f hf) ↔ ∀ i ∈ t, Disjoint s (f i)

theorem Finset.pairwiseDisjoint_disjUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {f g : α → Finset β} (hfg : ∀ (a : α), Disjoint (f a) (g a)) (hfg' : (↑s).Pairwise fun (a₁ a₂ : α) => Disjoint (f a₁) (g a₂)) (hf : (↑s).PairwiseDisjoint f) (hg : (↑s).PairwiseDisjoint g) : (↑s).PairwiseDisjoint fun (a : α) => (f a).disjUnion (g a) ⋯

theorem Finset.disjiUnion_disjUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {f g : α → Finset β} (hfg : ∀ (a : α), Disjoint (f a) (g a)) (hfg' : (↑s).Pairwise fun (a₁ a₂ : α) => Disjoint (f a₁) (g a₂)) (hf : (↑s).PairwiseDisjoint f) (hg : (↑s).PairwiseDisjoint g) : s.disjiUnion (fun (a : α) => (f a).disjUnion (g a) ⋯) ⋯ = (s.disjiUnion f hf).disjUnion (s.disjiUnion g hg) ⋯

def Finset.biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : α → Finset β) : Finset β

Finset.biUnion s t is the union of t a over a ∈ s.

(This was formerly bind due to the monad structure on types with DecidableEq.)

Equations

• s.biUnion t = (s.val.bind fun (a : α) => (t a).val).toFinset

@[simp]

theorem Finset.biUnion_val {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : α → Finset β) : (s.biUnion t).val = (s.val.bind fun (a : α) => (t a).val).dedup

@[simp]

theorem Finset.biUnion_empty {α : Type u_1} {β : Type u_2} {t : α → Finset β} [DecidableEq β] : ∅.biUnion t = ∅

@[simp]

theorem Finset.mem_biUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] {b : β} : b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a

@[simp]

theorem Finset.coe_biUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] : ↑(s.biUnion t) = ⋃ x ∈ ↑s, ↑(t x)

@[simp]

theorem Finset.biUnion_insert {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] [DecidableEq α] {a : α} : (insert a s).biUnion t = t a ∪ s.biUnion t

theorem Finset.biUnion_congr {α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} {t₁ t₂ : α → Finset β} [DecidableEq β] (hs : s₁ = s₂) (ht : ∀ a ∈ s₁, t₁ a = t₂ a) : s₁.biUnion t₁ = s₂.biUnion t₂

@[simp]

theorem Finset.disjiUnion_eq_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → Finset β) (hf : (↑s).PairwiseDisjoint f) : s.disjiUnion f hf = s.biUnion f

theorem Finset.biUnion_subset {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] {s' : Finset β} : s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'

@[simp]

theorem Finset.singleton_biUnion {α : Type u_1} {β : Type u_2} {t : α → Finset β} [DecidableEq β] {a : α} : {a}.biUnion t = t a

theorem Finset.biUnion_inter {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → Finset β) (t : Finset β) : s.biUnion f ∩ t = s.biUnion fun (x : α) => f x ∩ t

theorem Finset.inter_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (t : Finset β) (s : Finset α) (f : α → Finset β) : t ∩ s.biUnion f = s.biUnion fun (x : α) => t ∩ f x

theorem Finset.biUnion_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] (s : Finset α) (f : α → Finset β) (g : β → Finset γ) : (s.biUnion f).biUnion g = s.biUnion fun (a : α) => (f a).biUnion g

theorem Finset.bind_toFinset {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (s : Multiset α) (t : α → Multiset β) : (s.bind t).toFinset = s.toFinset.biUnion fun (a : α) => (t a).toFinset

theorem Finset.biUnion_mono {α : Type u_1} {β : Type u_2} {s : Finset α} {t₁ t₂ : α → Finset β} [DecidableEq β] (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) : s.biUnion t₁ ⊆ s.biUnion t₂

theorem Finset.biUnion_subset_biUnion_of_subset_left {α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} [DecidableEq β] (t : α → Finset β) (h : s₁ ⊆ s₂) : s₁.biUnion t ⊆ s₂.biUnion t

theorem Finset.subset_biUnion_of_mem {α : Type u_1} {β : Type u_2} {s : Finset α} [DecidableEq β] (u : α → Finset β) {x : α} (xs : x ∈ s) : u x ⊆ s.biUnion u

@[simp]

theorem Finset.biUnion_subset_iff_forall_subset {α : Type u_4} {β : Type u_5} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → Finset β} : s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t

@[simp]

theorem Finset.biUnion_singleton_eq_self {α : Type u_1} {s : Finset α} [DecidableEq α] : s.biUnion singleton = s

theorem Finset.filter_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → Finset β) (p : β → Prop) [DecidablePred p] : filter p (s.biUnion f) = s.biUnion fun (a : α) => filter p (f a)

theorem Finset.biUnion_filter_eq_of_maps_to {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {s : Finset α} {t : Finset β} {f : α → β} (h : ∀ x ∈ s, f x ∈ t) : (t.biUnion fun (a : β) => {c ∈ s | f c = a}) = s

theorem Finset.erase_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → Finset β) (s : Finset α) (b : β) : (s.biUnion f).erase b = s.biUnion fun (x : α) => (f x).erase b

@[simp]

theorem Finset.biUnion_nonempty {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] : (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty

theorem Finset.Nonempty.biUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] (hs : s.Nonempty) (ht : ∀ x ∈ s, (t x).Nonempty) : (s.biUnion t).Nonempty

theorem Finset.disjoint_biUnion_left {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → Finset β) (t : Finset β) : Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

theorem Finset.disjoint_biUnion_right {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset β) (t : Finset α) (f : α → Finset β) : Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)

theorem Finset.image_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {f : α → β} {s : Finset α} {t : β → Finset γ} : (image f s).biUnion t = s.biUnion fun (a : α) => t (f a)

theorem Finset.biUnion_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {s : Finset α} {t : α → Finset β} {f : β → γ} : image f (s.biUnion t) = s.biUnion fun (a : α) => image f (t a)

theorem Finset.image_biUnion_filter_eq {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (s : Finset β) (g : β → α) : ((image g s).biUnion fun (a : α) => {c ∈ s | g c = a}) = s

theorem Finset.union_biUnion {α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} {t : α → Finset β} [DecidableEq β] [DecidableEq α] : (s₁ ∪ s₂).biUnion t = s₁.biUnion t ∪ s₂.biUnion t

theorem Finset.biUnion_union {α : Type u_1} {β : Type u_2} {s : Finset α} {t₁ t₂ : α → Finset β} [DecidableEq β] : (s.biUnion fun (x : α) => t₁ x ∪ t₂ x) = s.biUnion t₁ ∪ s.biUnion t₂

theorem Finset.biUnion_singleton {α : Type u_1} {β : Type u_2} {s : Finset α} [DecidableEq β] {f : α → β} : (s.biUnion fun (a : α) => {f a}) = image f s

theorem Finset.attach_biUnion {α : Type u_1} {β : Type u_2} {s : Finset α} [DecidableEq β] {f : α → Finset β} : (s.attach.biUnion fun (x : ↥s) => f ↑x) = s.biUnion f

Rewrite a biUnion over s.attach as a biUnion over s, in the case where the indexing function on s.attach happens to factor through α. See Finset.attach_biUnion' for the version without that hypothesis.

theorem Finset.attach_biUnion' {α : Type u_1} {β : Type u_2} {s : Finset α} [DecidableEq β] [DecidableEq α] {f : ↥s → Finset β} : s.attach.biUnion f = s.biUnion fun (a : α) => if h : a ∈ s then f ⟨a, h⟩ else ∅

Rewrite a biUnion over s.attach as a biUnion over s by extending the function to all of α with ∅ outside s. See Finset.attach_biUnion for the version when the indexing function is already defined on all of α.