# 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 : ) (t : α) (hf : (s).PairwiseDisjoint t) :

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 := }
Instances For
@[simp]
theorem Finset.disjiUnion_val {α : Type u_1} {β : Type u_2} (s : ) (t : α) (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 : α) :
.disjiUnion t =
@[simp]
theorem Finset.mem_disjiUnion {α : Type u_1} {β : Type u_2} {s : } {t : α} {b : β} {h : (s).PairwiseDisjoint t} :
b s.disjiUnion t h as, b t a
@[simp]
theorem Finset.coe_disjiUnion {α : Type u_1} {β : Type u_2} {s : } {t : α} {h : (s).PairwiseDisjoint t} :
(s.disjiUnion t h) = xs, (t x)
@[simp]
theorem Finset.disjiUnion_cons {α : Type u_1} {β : Type u_2} (a : α) (s : ) (ha : as) (f : α) (H : ((Finset.cons a s ha)).PairwiseDisjoint f) :
(Finset.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 : α} (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 : ) (f : α) (g : β) (h1 : (s).PairwiseDisjoint f) (h2 : ((s.disjiUnion f h1)).PairwiseDisjoint g) :
(s.disjiUnion f h1).disjiUnion g h2 = s.attach.disjiUnion (fun (a : { x : α // x s }) => (f a).disjiUnion g )
@[simp]
theorem Finset.disjiUnion_filter_eq {α : Type u_1} {β : Type u_2} [] (s : ) (t : ) (f : αβ) :
t.disjiUnion (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} [] {s : } {t : } {f : αβ} (h : xs, f x t) :
t.disjiUnion (fun (a : β) => Finset.filter (fun (x : α) => f x = a) s) = s
def Finset.biUnion {α : Type u_1} {β : Type u_2} [] (s : ) (t : α) :

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
Instances For
@[simp]
theorem Finset.biUnion_val {α : Type u_1} {β : Type u_2} [] (s : ) (t : α) :
(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 : α} [] :
.biUnion t =
@[simp]
theorem Finset.mem_biUnion {α : Type u_1} {β : Type u_2} {s : } {t : α} [] {b : β} :
b s.biUnion t as, b t a
@[simp]
theorem Finset.coe_biUnion {α : Type u_1} {β : Type u_2} {s : } {t : α} [] :
(s.biUnion t) = xs, (t x)
@[simp]
theorem Finset.biUnion_insert {α : Type u_1} {β : Type u_2} {s : } {t : α} [] [] {a : α} :
(insert a s).biUnion t = t a s.biUnion t
theorem Finset.biUnion_congr {α : Type u_1} {β : Type u_2} {s₁ : } {s₂ : } {t₁ : α} {t₂ : α} [] (hs : s₁ = s₂) (ht : as₁, t₁ a = t₂ a) :
s₁.biUnion t₁ = s₂.biUnion t₂
@[simp]
theorem Finset.disjiUnion_eq_biUnion {α : Type u_1} {β : Type u_2} [] (s : ) (f : α) (hf : (s).PairwiseDisjoint f) :
s.disjiUnion f hf = s.biUnion f
theorem Finset.biUnion_subset {α : Type u_1} {β : Type u_2} {s : } {t : α} [] {s' : } :
s.biUnion t s' xs, t x s'
@[simp]
theorem Finset.singleton_biUnion {α : Type u_1} {β : Type u_2} {t : α} [] {a : α} :
{a}.biUnion t = t a
theorem Finset.biUnion_inter {α : Type u_1} {β : Type u_2} [] (s : ) (f : α) (t : ) :
s.biUnion f t = s.biUnion fun (x : α) => f x t
theorem Finset.inter_biUnion {α : Type u_1} {β : Type u_2} [] (t : ) (s : ) (f : α) :
t s.biUnion f = s.biUnion fun (x : α) => t f x
theorem Finset.biUnion_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (s : ) (f : α) (g : β) :
(s.biUnion f).biUnion g = s.biUnion fun (a : α) => (f a).biUnion g
theorem Finset.bind_toFinset {α : Type u_1} {β : Type u_2} [] [] (s : ) (t : α) :
(s.bind t).toFinset = s.toFinset.biUnion fun (a : α) => (t a).toFinset
theorem Finset.biUnion_mono {α : Type u_1} {β : Type u_2} {s : } {t₁ : α} {t₂ : α} [] (h : as, 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₂ : } [] (t : α) (h : s₁ s₂) :
s₁.biUnion t s₂.biUnion t
theorem Finset.subset_biUnion_of_mem {α : Type u_1} {β : Type u_2} {s : } [] (u : α) {x : α} (xs : x s) :
u x s.biUnion u
@[simp]
theorem Finset.biUnion_subset_iff_forall_subset {α : Type u_4} {β : Type u_5} [] {s : } {t : } {f : α} :
s.biUnion f t xs, f x t
@[simp]
theorem Finset.biUnion_singleton_eq_self {α : Type u_1} {s : } [] :
s.biUnion singleton = s
theorem Finset.filter_biUnion {α : Type u_1} {β : Type u_2} [] (s : ) (f : α) (p : βProp) [] :
Finset.filter p (s.biUnion f) = s.biUnion fun (a : α) => Finset.filter p (f a)
theorem Finset.biUnion_filter_eq_of_maps_to {α : Type u_1} {β : Type u_2} [] [] {s : } {t : } {f : αβ} (h : xs, f x t) :
(t.biUnion fun (a : β) => Finset.filter (fun (c : α) => f c = a) s) = s
theorem Finset.erase_biUnion {α : Type u_1} {β : Type u_2} [] (f : α) (s : ) (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 : } {t : α} [] :
(s.biUnion t).Nonempty xs, (t x).Nonempty
theorem Finset.Nonempty.biUnion {α : Type u_1} {β : Type u_2} {s : } {t : α} [] (hs : s.Nonempty) (ht : xs, (t x).Nonempty) :
(s.biUnion t).Nonempty
theorem Finset.disjoint_biUnion_left {α : Type u_1} {β : Type u_2} [] (s : ) (f : α) (t : ) :
Disjoint (s.biUnion f) t is, Disjoint (f i) t
theorem Finset.disjoint_biUnion_right {α : Type u_1} {β : Type u_2} [] (s : ) (t : ) (f : α) :
Disjoint s (t.biUnion f) it, Disjoint s (f i)