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 : Set.PairwiseDisjoint (↑s) 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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Finset.coe_disjiUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} {h : Set.PairwiseDisjoint (↑s) t} : ↑(Finset.disjiUnion s 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 : Set.PairwiseDisjoint (↑(Finset.cons a s ha)) f) : Finset.disjiUnion (Finset.cons a s ha) f H = Finset.disjUnion (f a) (Finset.disjiUnion s f ⋯) ⋯

@[simp]

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

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

@[simp]

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

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) : Finset.disjiUnion t (fun (a : β) => Finset.filter (fun (x : α) => f x = a) s) ⋯ = s

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

theorem Finset.inter_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (t : Finset β) (s : Finset α) (f : α → Finset β) : t ∩ Finset.biUnion s f = Finset.biUnion s 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 γ) : Finset.biUnion (Finset.biUnion s f) g = Finset.biUnion s fun (a : α) => Finset.biUnion (f a) g

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

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

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

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

@[simp]

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

@[simp]

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

theorem Finset.filter_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → Finset β) (p : β → Prop) [DecidablePred p] : Finset.filter p (Finset.biUnion s f) = Finset.biUnion s fun (a : α) => Finset.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) : (Finset.biUnion t fun (a : β) => Finset.filter (fun (c : α) => f c = a) s) = s

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

@[simp]

theorem Finset.biUnion_nonempty {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] : (Finset.biUnion s 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) : (Finset.biUnion s t).Nonempty

theorem Finset.disjoint_biUnion_left {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → Finset β) (t : Finset β) : Disjoint (Finset.biUnion s 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 (Finset.biUnion t f) ↔ ∀ i ∈ t, Disjoint s (f i)