Mathlib.Data.Finset.Union

Finset.disjiUnion definition

(s : Finset α) (t : α → Finset β) (hf : (s : Set α).PairwiseDisjoint t) : Finset β

Full source

/-- `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. -/
def disjiUnion (s : Finset α) (t : α → Finset β) (hf : (s : Set α).PairwiseDisjoint t) : Finset β :=
  ⟨s.val.bind (Finset.val ∘ t), Multiset.nodup_bind.2
    ⟨fun a _ ↦ (t a).nodup, s.nodup.pairwise fun _ ha _ hb hab ↦ disjoint_val.2 <| hf ha hb hab⟩⟩

Disjoint union of finite sets

Informal description

Given a finite set $s$ of type $\alpha$ and a function $t \colon \alpha \to \text{Finset} \beta$ such that the images $t(a)$ for $a \in s$ are pairwise disjoint, the finite set $\text{disjiUnion}(s, t, hf)$ consists of all elements $b \in \beta$ such that $b \in t(a)$ for some $a \in s$. More formally, $\text{disjiUnion}(s, t, hf)$ is the finite set whose underlying multiset is the union (bind) of the multisets corresponding to $t(a)$ for all $a \in s$, with the disjointness condition ensuring no duplicates in the union.

Finset.disjiUnion_val theorem

(s : Finset α) (t : α → Finset β) (h) : (s.disjiUnion t h).1 = s.1.bind fun a ↦ (t a).1

Full source

@[simp]
lemma disjiUnion_val (s : Finset α) (t : α → Finset β) (h) :
    (s.disjiUnion t h).1 = s.1.bind fun a ↦ (t a).1 := rfl

Underlying multiset of disjoint union equals multiset bind

Informal description

For any finite set $s$ of type $\alpha$ and any function $t \colon \alpha \to \text{Finset} \beta$ such that the images $t(a)$ for $a \in s$ are pairwise disjoint, the underlying multiset of the disjoint union $\text{disjUnion}(s, t, h)$ is equal to the multiset bind operation applied to the underlying multiset of $s$ and the function mapping each $a$ to the underlying multiset of $t(a)$. More formally, if $\text{val}(X)$ denotes the underlying multiset of a finite set $X$, then: \[ \text{val}(\text{disjUnion}(s, t, h)) = \text{bind}(\text{val}(s), \lambda a, \text{val}(t(a))) \]

Finset.disjiUnion_empty theorem

(t : α → Finset β) : disjiUnion ∅ t (by simp) = ∅

Full source

@[simp] lemma disjiUnion_empty (t : α → Finset β) : disjiUnion ∅ t (by simp) = ∅ := rfl

Empty Disjoint Union of Finite Sets: $\text{disjiUnion}(\emptyset, t) = \emptyset$

Informal description

For any function $t \colon \alpha \to \text{Finset} \beta$, the disjoint union of the empty finite set $\emptyset$ with $t$ is equal to the empty finite set $\emptyset$.

Finset.mem_disjiUnion theorem

{b : β} {h} : b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a

Full source

@[simp] lemma mem_disjiUnion {b : β} {h} : b ∈ s.disjiUnion t hb ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a := by
  simp only [mem_def, disjiUnion_val, Multiset.mem_bind, exists_prop]

Membership in Disjoint Union of Finite Sets

Informal description

For any element $b \in \beta$ and any finite set $s \subseteq \alpha$ with a function $t \colon \alpha \to \text{Finset} \beta$ such that the images $t(a)$ for $a \in s$ are pairwise disjoint, we have $b \in \text{disjUnion}(s, t, h)$ if and only if there exists an element $a \in s$ such that $b \in t(a)$.

Finset.coe_disjiUnion theorem

{h} : (s.disjiUnion t h : Set β) = ⋃ x ∈ (s : Set α), t x

Full source

@[simp, norm_cast]
lemma coe_disjiUnion {h} : (s.disjiUnion t h : Set β) = ⋃ x ∈ (s : Set α), t x := by
  simp [Set.ext_iff, mem_disjiUnion, Set.mem_iUnion, mem_coe, imp_true_iff]

Underlying Set of Disjoint Union Equals Union of Images

Informal description

For a finite set $s$ of type $\alpha$ and a function $t \colon \alpha \to \text{Finset} \beta$ such that the images $t(a)$ for $a \in s$ are pairwise disjoint, the underlying set of the disjoint union $\text{disjiUnion}(s, t, h)$ is equal to the union of all sets $t(x)$ for $x$ in the underlying set of $s$. More formally, we have: $$ \text{disjiUnion}(s, t, h) = \bigcup_{x \in s} t(x) $$

Finset.disjiUnion_cons theorem

 (a : α) (s : Finset α) (ha : a ∉ s) (f : α → Finset β) (H) :
  disjiUnion (cons a s ha) f H =
    (f a).disjUnion ((s.disjiUnion f) fun _ hb _ hc ↦ H (mem_cons_of_mem hb) (mem_cons_of_mem hc))
      (disjoint_left.2 fun _ hb h ↦
        let ⟨_, hc, h⟩ := mem_disjiUnion.mp h
        disjoint_left.mp (H (mem_cons_self a s) (mem_cons_of_mem hc) (ne_of_mem_of_not_mem hc ha).symm) hb h)

Full source

@[simp] lemma disjiUnion_cons (a : α) (s : Finset α) (ha : a ∉ s) (f : α → Finset β) (H) :
    disjiUnion (cons a s ha) f H =
    (f a).disjUnion ((s.disjiUnion f) fun _ hb _ hc ↦ H (mem_cons_of_mem hb) (mem_cons_of_mem hc))
      (disjoint_left.2 fun _ hb h ↦
        let ⟨_, hc, h⟩ := mem_disjiUnion.mp h
        disjoint_left.mp
          (H (mem_cons_self a s) (mem_cons_of_mem hc) (ne_of_mem_of_not_mem hc ha).symm) hb h) :=
  eq_of_veq <| Multiset.cons_bind _ _ _

Disjoint Union Decomposition: $\text{disjiUnion}(\text{cons}(a, s, ha), f) = f(a) \sqcup \text{disjiUnion}(s, f)$

Informal description

Let $a$ be an element of type $\alpha$, $s$ a finite subset of $\alpha$ such that $a \notin s$, and $f \colon \alpha \to \text{Finset} \beta$ a function such that the images $f(x)$ for $x \in \text{cons}(a, s, ha)$ are pairwise disjoint. Then the disjoint union of $f$ over $\text{cons}(a, s, ha)$ is equal to the disjoint union of $f(a)$ with the disjoint union of $f$ over $s$. More formally, we have: \[ \text{disjiUnion}(\text{cons}(a, s, ha), f, H) = f(a) \sqcup \text{disjiUnion}(s, f, H'), \] where $H'$ ensures that the images $f(x)$ for $x \in s$ remain pairwise disjoint under the extended condition, and $\sqcup$ denotes the disjoint union operation.

Finset.singleton_disjiUnion theorem

(a : α) {h} : Finset.disjiUnion { a } t h = t a

Full source

@[simp] lemma singleton_disjiUnion (a : α) {h} : Finset.disjiUnion {a} t h = t a :=
  eq_of_veq <| Multiset.singleton_bind _ _

Disjoint Union of Singleton Finite Set: $\text{disjiUnion}(\{a\}, t, h) = t(a)$

Informal description

For any element $a$ of type $\alpha$ and any function $t \colon \alpha \to \text{Finset} \beta$ such that the images of $t$ on the singleton set $\{a\}$ are pairwise disjoint, the disjoint union $\text{disjiUnion}(\{a\}, t, h)$ is equal to $t(a)$.

Finset.disjiUnion_disjiUnion theorem

 (s : Finset α) (f : α → Finset β) (g : β → Finset γ) (h1 h2) :
  (s.disjiUnion f h1).disjiUnion g h2 =
    s.attach.disjiUnion
      (fun a ↦
        ((f a).disjiUnion g) fun _ hb _ hc ↦
          h2 (mem_disjiUnion.mpr ⟨_, a.prop, hb⟩) (mem_disjiUnion.mpr ⟨_, a.prop, hc⟩))
      fun a _ b _ hab ↦
      disjoint_left.mpr fun x hxa hxb ↦
        by
        obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa
        obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb
        refine
          disjoint_left.mp (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) ?_) hga hgb
        rintro rfl
        exact disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb

Full source

lemma disjiUnion_disjiUnion (s : Finset α) (f : α → Finset β) (g : β → Finset γ) (h1 h2) :
    (s.disjiUnion f h1).disjiUnion g h2 =
      s.attach.disjiUnion
        (fun a ↦ ((f a).disjiUnion g) fun _ hb _ hc ↦
            h2 (mem_disjiUnion.mpr ⟨_, a.prop, hb⟩) (mem_disjiUnion.mpr ⟨_, a.prop, hc⟩))
        fun a _ b _ hab ↦
        disjoint_left.mpr fun x hxa hxb ↦ by
          obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa
          obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb
          refine disjoint_left.mp
            (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) ?_) hga
            hgb
          rintro rfl
          exact disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb :=
  eq_of_veq <| Multiset.bind_assoc.trans (Multiset.attach_bind_coe _ _).symm

Associativity of Iterated Disjoint Union of Finite Sets

Informal description

Let $s$ be a finite set of type $\alpha$, $f \colon \alpha \to \text{Finset} \beta$ a function such that the images $f(a)$ for $a \in s$ are pairwise disjoint (with proof $h_1$), and $g \colon \beta \to \text{Finset} \gamma$ a function such that the images $g(b)$ for $b \in \text{disjUnion}(s, f, h_1)$ are pairwise disjoint (with proof $h_2)$. Then the iterated disjoint union $\text{disjUnion}(\text{disjUnion}(s, f, h_1), g, h_2)$ is equal to the disjoint union of $s$'s attached elements, where each element $a \in s$ is mapped to $\text{disjUnion}(f(a), g, \text{conditions})$, with appropriate disjointness conditions. More precisely, the equality states: \[ \text{disjUnion}(\text{disjUnion}(s, f, h_1), g, h_2) = \text{disjUnion}(s.\text{attach}, \lambda a, \text{disjUnion}(f(a), g, \text{conditions}), \text{disjointness proof}). \]

Finset.sUnion_disjiUnion theorem

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

Full source

lemma sUnion_disjiUnion {f : α → Finset (Set β)} (I : Finset α)
    (hf : (I : Set α).PairwiseDisjoint f) :
    ⋃₀ (I.disjiUnion f hf : Set (Set β)) = ⋃ a ∈ I, ⋃₀ ↑(f a) := by
  ext
  simp only [coe_disjiUnion, Set.mem_sUnion, Set.mem_iUnion, mem_coe, exists_prop]
  tauto

Union of Disjoint Union of Finite Sets of Sets

Informal description

For any finite set $I$ of type $\alpha$ and any function $f \colon \alpha \to \text{Finset}(\text{Set} \beta)$ such that the images $f(a)$ for $a \in I$ are pairwise disjoint, the union of all sets in the disjoint union $\text{disjUnion}(I, f, hf)$ is equal to the union over all $a \in I$ of the unions of the sets in $f(a)$. More formally, we have: $$ \bigcup_{S \in \text{disjUnion}(I, f, hf)} S = \bigcup_{a \in I} \bigcup_{T \in f(a)} T $$

Finset.disjiUnion_filter_eq theorem

 (s : Finset α) (t : Finset β) (f : α → β) :
  t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers = s.filter fun c ↦ f c ∈ t

Full source

@[simp] lemma disjiUnion_filter_eq (s : Finset α) (t : Finset β) (f : α → β) :
    t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers =
      s.filter fun c ↦ f c ∈ t :=
  ext fun b => by simpa using and_comm

Equality of Disjoint Union of Fibers and Preimage Filter

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any function $f \colon \alpha \to \beta$, the disjoint union of the filtered sets $\{x \in s \mid f(x) = a\}$ over all $a \in t$ is equal to the filtered set $\{x \in s \mid f(x) \in t\}$. More precisely, given $s$, $t$, and $f$ as above, we have: \[ \bigsqcup_{a \in t} \{x \in s \mid f(x) = a\} = \{x \in s \mid f(x) \in t\} \] where $\bigsqcup$ denotes the disjoint union operation.

Finset.disjiUnion_filter_eq_of_maps_to theorem

(h : ∀ x ∈ s, f x ∈ t) : t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers = s

Full source

lemma disjiUnion_filter_eq_of_maps_to (h : ∀ x ∈ s, f x ∈ t) :
    t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers = s := by
  simpa [filter_eq_self]

Disjoint Union of Fibers Equals Original Set Under Mapping Condition

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any function $f \colon \alpha \to \beta$ such that $f(x) \in t$ for all $x \in s$, the disjoint union of the fibers $\{x \in s \mid f(x) = a\}$ over all $a \in t$ equals $s$. More precisely: \[ \bigsqcup_{a \in t} \{x \in s \mid f(x) = a\} = s \] where $\bigsqcup$ denotes the disjoint union operation.

Finset.map_disjiUnion theorem

 {f : α ↪ β} {s : Finset α} {t : β → Finset γ} {h} :
  (s.map f).disjiUnion t h =
    s.disjiUnion (fun a => t (f a)) fun _ ha _ hb hab =>
      h (mem_map_of_mem _ ha) (mem_map_of_mem _ hb) (f.injective.ne hab)

Full source

theorem map_disjiUnion {f : α ↪ β} {s : Finset α} {t : β → Finset γ} {h} :
    (s.map f).disjiUnion t h =
      s.disjiUnion (fun a => t (f a)) fun _ ha _ hb hab =>
        h (mem_map_of_mem _ ha) (mem_map_of_mem _ hb) (f.injective.ne hab) :=
  eq_of_veq <| Multiset.bind_map _ _ _

Commutativity of Map and Disjoint Union for Finite Sets

Informal description

Let $f \colon \alpha \hookrightarrow \beta$ be an injective function, $s$ a finite subset of $\alpha$, and $t \colon \beta \to \text{Finset} \gamma$ a function such that the images $t(b)$ for $b \in s.map(f)$ are pairwise disjoint. Then the disjoint union of $t$ over $s.map(f)$ is equal to the disjoint union of $t \circ f$ over $s$, where the disjointness condition for the latter is derived from the injectivity of $f$ and the pairwise disjointness of $t$ on $s.map(f)$. More formally: \[ \text{disjUnion}(s.map(f), t, h) = \text{disjUnion}(s, t \circ f, h') \] where $h'$ is the condition that for any distinct $a_1, a_2 \in s$, the sets $t(f(a_1))$ and $t(f(a_2))$ are disjoint, which follows from $h$ and the injectivity of $f$.

Finset.disjiUnion_map theorem

 {s : Finset α} {t : α → Finset β} {f : β ↪ γ} {h} :
  (s.disjiUnion t h).map f = s.disjiUnion (fun a => (t a).map f) (h.mono' fun _ _ ↦ (disjoint_map _).2)

Full source

theorem disjiUnion_map {s : Finset α} {t : α → Finset β} {f : β ↪ γ} {h} :
    (s.disjiUnion t h).map f =
      s.disjiUnion (fun a => (t a).map f) (h.mono' fun _ _ ↦ (disjoint_map _).2) :=
  eq_of_veq <| Multiset.map_bind _ _ _

Image of Disjoint Union under Injective Function Equals Disjoint Union of Images

Informal description

Let $s$ be a finite set of type $\alpha$, $t \colon \alpha \to \text{Finset} \beta$ a function such that the images $t(a)$ for $a \in s$ are pairwise disjoint, and $f \colon \beta \hookrightarrow \gamma$ an injective function. Then the image of the disjoint union $\text{disjUnion}(s, t, h)$ under $f$ is equal to the disjoint union of the images of $t(a)$ under $f$ for $a \in s$, i.e., \[ f\left(\bigsqcup_{a \in s} t(a)\right) = \bigsqcup_{a \in s} f(t(a)). \] Here, the disjointness condition for the right-hand side is derived from the injectivity of $f$ and the pairwise disjointness of the $t(a)$.

Finset.fold_disjiUnion theorem

 {ι : Type*} {s : Finset ι} {t : ι → Finset α} {b : ι → β} {b₀ : β} (h) :
  (s.disjiUnion t h).fold op (s.fold op b₀ b) f = s.fold op b₀ fun i => (t i).fold op (b i) f

Full source

theorem fold_disjiUnion {ι : Type*} {s : Finset ι} {t : ι → Finset α} {b : ι → β} {b₀ : β} (h) :
    (s.disjiUnion t h).fold op (s.fold op b₀ b) f = s.fold op b₀ fun i => (t i).fold op (b i) f :=
  (congr_arg _ <| Multiset.map_bind _ _ _).trans (Multiset.fold_bind _ _ _ _ _)

Distributivity of Fold over Disjoint Union: $\text{fold}\, \text{op}\, (\text{fold}\, \text{op}\, b_0\, b\, s)\, f\, (\text{disjiUnion}\, s\, t\, h) = \text{fold}\, \text{op}\, b_0\, (\lambda i, \text{fold}\, \text{op}\, (b i)\, f\, (t i))\, s$

Informal description

Let $\iota$ and $\alpha$ be types, and let $s$ be a finite set of elements of type $\iota$. Given a function $t \colon \iota \to \text{Finset} \alpha$ such that the images $t(i)$ for $i \in s$ are pairwise disjoint, a commutative and associative binary operation $\text{op} \colon \beta \to \beta \to \beta$, functions $b \colon \iota \to \beta$ and $f \colon \alpha \to \beta$, and an initial value $b_0 \in \beta$, the following equality holds: \[ \text{fold}\, \text{op}\, \left(\text{fold}\, \text{op}\, b_0\, b\, s\right)\, f\, (\text{disjiUnion}\, s\, t\, h) = \text{fold}\, \text{op}\, b_0\, \left(\lambda i, \text{fold}\, \text{op}\, (b i)\, f\, (t i)\right)\, s. \] Here, $\text{disjiUnion}\, s\, t\, h$ denotes the disjoint union of the finite sets $t(i)$ for $i \in s$, and $\text{fold}\, \text{op}\, b_0\, f\, s$ denotes the fold of the finite set $s$ with operation $\text{op}$, initial value $b_0$, and function $f$.

Finset.biUnion definition

(s : Finset α) (t : α → Finset β) : Finset β

Full source

/-- `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`.) -/
protected def biUnion (s : Finset α) (t : α → Finset β) : Finset β :=
  (s.1.bind fun a ↦ (t a).1).toFinset

Finite union of finite sets

Informal description

Given a finite set $s$ of type $\alpha$ and a function $t : \alpha \to \text{Finset} \beta$, the finite union $\text{biUnion}(s, t)$ is the union of all finite sets $t(a)$ for $a \in s$. This is implemented as the deduplicated multiset formed by binding the function $t$ over the underlying multiset of $s$.

Finset.biUnion_val theorem

(s : Finset α) (t : α → Finset β) : (s.biUnion t).1 = (s.1.bind fun a ↦ (t a).1).dedup

Full source

@[simp] lemma biUnion_val (s : Finset α) (t : α → Finset β) :
    (s.biUnion t).1 = (s.1.bind fun a ↦ (t a).1).dedup := rfl

Underlying Multiset of Finite Union Equals Deduplicated Bind

Informal description

For any finite set $s$ of type $\alpha$ and any function $t : \alpha \to \text{Finset} \beta$, the underlying multiset of the finite union $\text{biUnion}(s, t)$ is equal to the deduplicated version of the multiset obtained by binding the function $\lambda a, (t a).1$ over the underlying multiset of $s$.

Finset.biUnion_empty theorem

: Finset.biUnion ∅ t = ∅

Full source

@[simp] lemma biUnion_empty : Finset.biUnion ∅ t = ∅ := rfl

Empty Set Union Property: $\text{biUnion}(\emptyset, t) = \emptyset$

Informal description

For any function $t : \alpha \to \text{Finset} \beta$, the finite union of the empty set $\emptyset$ with respect to $t$ is equal to the empty set, i.e., $\text{biUnion}(\emptyset, t) = \emptyset$.

Finset.mem_biUnion theorem

{b : β} : b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a

Full source

@[simp] lemma mem_biUnion {b : β} : b ∈ s.biUnion tb ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a := by
  simp only [mem_def, biUnion_val, Multiset.mem_dedup, Multiset.mem_bind, exists_prop]

Membership in Finite Union of Finite Sets

Informal description

For any element $b$ of type $\beta$, $b$ belongs to the finite union $\text{biUnion}(s, t)$ if and only if there exists an element $a \in s$ such that $b \in t(a)$.

Finset.coe_biUnion theorem

: (s.biUnion t : Set β) = ⋃ x ∈ (s : Set α), t x

Full source

@[simp, norm_cast]
lemma coe_biUnion : (s.biUnion t : Set β) = ⋃ x ∈ (s : Set α), t x := by
  simp [Set.ext_iff, mem_biUnion, Set.mem_iUnion, mem_coe, imp_true_iff]

Equality between Finite Union and Indexed Union of Sets

Informal description

For a finite set $s$ of type $\alpha$ and a function $t : \alpha \to \text{Finset} \beta$, the underlying set of the finite union $\text{biUnion}(s, t)$ is equal to the indexed union $\bigcup_{x \in s} t(x)$.

Finset.biUnion_insert theorem

[DecidableEq α] {a : α} : (insert a s).biUnion t = t a ∪ s.biUnion t

Full source

@[simp]
lemma biUnion_insert [DecidableEq α] {a : α} : (insert a s).biUnion t = t a ∪ s.biUnion t := by
  aesop

Finite Union over Insertion Equals Union with Singleton: $\text{biUnion}(\{a\} \cup s, t) = t(a) \cup \text{biUnion}(s, t)$

Informal description

For any finite set $s$ of type $\alpha$ with decidable equality, any element $a \in \alpha$, and any function $t : \alpha \to \text{Finset} \beta$, the finite union of $t$ over the insertion of $a$ into $s$ is equal to the union of $t(a)$ with the finite union of $t$ over $s$. That is, \[ \text{biUnion}(\{a\} \cup s, t) = t(a) \cup \text{biUnion}(s, t). \]

Finset.biUnion_congr theorem

(hs : s₁ = s₂) (ht : ∀ a ∈ s₁, t₁ a = t₂ a) : s₁.biUnion t₁ = s₂.biUnion t₂

Full source

lemma biUnion_congr (hs : s₁ = s₂) (ht : ∀ a ∈ s₁, t₁ a = t₂ a) :
    s₁.biUnion t₁ = s₂.biUnion t₂ := by
  aesop

Congruence of Finite Unions under Equal Index Sets and Pointwise Equal Functions

Informal description

Let $s_1$ and $s_2$ be finite sets of type $\alpha$, and let $t_1, t_2 : \alpha \to \text{Finset} \beta$ be functions mapping elements of $\alpha$ to finite sets of type $\beta$. If $s_1 = s_2$ and for every $a \in s_1$, $t_1(a) = t_2(a)$, then the finite unions $\bigcup_{a \in s_1} t_1(a)$ and $\bigcup_{a \in s_2} t_2(a)$ are equal.

Finset.disjiUnion_eq_biUnion theorem

(s : Finset α) (f : α → Finset β) (hf) : s.disjiUnion f hf = s.biUnion f

Full source

@[simp]
lemma disjiUnion_eq_biUnion (s : Finset α) (f : α → Finset β) (hf) :
    s.disjiUnion f hf = s.biUnion f := eq_of_veq (s.disjiUnion f hf).nodup.dedup.symm

Disjoint Union Equals Finite Union under Pairwise Disjointness: $\text{disjiUnion}(s, f, hf) = \text{biUnion}(s, f)$

Informal description

For any finite set $s$ of type $\alpha$ and any function $f : \alpha \to \text{Finset} \beta$, if the images $f(a)$ for $a \in s$ are pairwise disjoint, then the disjoint union $\text{disjiUnion}(s, f, hf)$ is equal to the finite union $\text{biUnion}(s, f)$.

Finset.biUnion_subset theorem

{s' : Finset β} : s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'

Full source

lemma biUnion_subset {s' : Finset β} : s.biUnion t ⊆ s's.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s' := by
  simp only [subset_iff, mem_biUnion]
  exact ⟨fun H a ha b hb ↦ H ⟨a, ha, hb⟩, fun H b ⟨a, ha, hb⟩ ↦ H a ha hb⟩

Characterization of Finite Union Subset via Pointwise Subsets

Informal description

For any finite set $s'$ of type $\beta$, the finite union $\bigcup_{x \in s} t(x)$ is a subset of $s'$ if and only if for every element $x$ in $s$, the finite set $t(x)$ is a subset of $s'$. In other words: \[ \left(\bigcup_{x \in s} t(x)\right) \subseteq s' \leftrightarrow \forall x \in s, \, t(x) \subseteq s'. \]

Finset.singleton_biUnion theorem

{a : α} : Finset.biUnion { a } t = t a

Full source

@[simp]
lemma singleton_biUnion {a : α} : Finset.biUnion {a} t = t a := by
  classical rw [← insert_empty_eq, biUnion_insert, biUnion_empty, union_empty]

Finite Union over Singleton Equals Function Value: $\bigcup_{x \in \{a\}} t(x) = t(a)$

Informal description

For any element $a$ of type $\alpha$ and any function $t : \alpha \to \text{Finset} \beta$, the finite union of $t$ over the singleton set $\{a\}$ is equal to $t(a)$. That is, \[ \bigcup_{x \in \{a\}} t(x) = t(a). \]

Finset.biUnion_inter theorem

(s : Finset α) (f : α → Finset β) (t : Finset β) : s.biUnion f ∩ t = s.biUnion fun x ↦ f x ∩ t

Full source

lemma biUnion_inter (s : Finset α) (f : α → Finset β) (t : Finset β) :
    s.biUnion f ∩ t = s.biUnion fun x ↦ f x ∩ t := by
  ext x
  simp only [mem_biUnion, mem_inter]
  tauto

Distributivity of Intersection over Finite Union: $\left(\bigcup_{x \in s} f(x)\right) \cap t = \bigcup_{x \in s} (f(x) \cap t)$

Informal description

For any finite set $s$ of type $\alpha$, a function $f : \alpha \to \text{Finset} \beta$, and a finite set $t$ of type $\beta$, the intersection of the finite union $\bigcup_{x \in s} f(x)$ with $t$ is equal to the finite union of the intersections $\bigcup_{x \in s} (f(x) \cap t)$. In other words: \[ \left(\bigcup_{x \in s} f(x)\right) \cap t = \bigcup_{x \in s} (f(x) \cap t). \]

Finset.inter_biUnion theorem

(t : Finset β) (s : Finset α) (f : α → Finset β) : t ∩ s.biUnion f = s.biUnion fun x ↦ t ∩ f x

Full source

lemma inter_biUnion (t : Finset β) (s : Finset α) (f : α → Finset β) :
    t ∩ s.biUnion f = s.biUnion fun x ↦ t ∩ f x := by
  rw [inter_comm, biUnion_inter]
  simp [inter_comm]

Distributivity of Intersection over Finite Union (Symmetric Version)

Informal description

For any finite set $t$ of type $\beta$, a finite set $s$ of type $\alpha$, and a function $f : \alpha \to \text{Finset} \beta$, the intersection of $t$ with the finite union $\bigcup_{x \in s} f(x)$ is equal to the finite union of the intersections $\bigcup_{x \in s} (t \cap f(x))$. In other words: \[ t \cap \left(\bigcup_{x \in s} f(x)\right) = \bigcup_{x \in s} (t \cap f(x)). \]

Finset.biUnion_biUnion theorem

 [DecidableEq γ] (s : Finset α) (f : α → Finset β) (g : β → Finset γ) :
  (s.biUnion f).biUnion g = s.biUnion fun a ↦ (f a).biUnion g

Full source

lemma biUnion_biUnion [DecidableEq γ] (s : Finset α) (f : α → Finset β) (g : β → Finset γ) :
    (s.biUnion f).biUnion g = s.biUnion fun a ↦ (f a).biUnion g := by
  ext
  simp only [Finset.mem_biUnion, exists_prop]
  simp_rw [← exists_and_right, ← exists_and_left, and_assoc]
  rw [exists_comm]

Associativity of Finite Unions: $\bigcup_{a \in s} \bigcup_{b \in f(a)} g(b) = \bigcup_{b \in \bigcup_{a \in s} f(a)} g(b)$

Informal description

Let $s$ be a finite set of type $\alpha$, $f : \alpha \to \text{Finset} \beta$ a function mapping elements of $\alpha$ to finite sets of $\beta$, and $g : \beta \to \text{Finset} \gamma$ a function mapping elements of $\beta$ to finite sets of $\gamma$. Then the double finite union satisfies: \[ \left(\bigcup_{a \in s} f(a)\right) \bigcup_{b \in \bigcup_{a \in s} f(a)} g(b) = \bigcup_{a \in s} \left( \bigcup_{b \in f(a)} g(b) \right) \]

Finset.bind_toFinset theorem

 [DecidableEq α] (s : Multiset α) (t : α → Multiset β) : (s.bind t).toFinset = s.toFinset.biUnion fun a ↦ (t a).toFinset

Full source

lemma bind_toFinset [DecidableEq α] (s : Multiset α) (t : α → Multiset β) :
    (s.bind t).toFinset = s.toFinset.biUnion fun a ↦ (t a).toFinset :=
  ext fun x ↦ by simp only [Multiset.mem_toFinset, mem_biUnion, Multiset.mem_bind, exists_prop]

Equality of Finset Conversion and Finite Union of Multiset Bind

Informal description

For a multiset $s$ over a type $\alpha$ with decidable equality and a function $t : \alpha \to \text{Multiset} \beta$, the finite set obtained by converting the bind of $s$ and $t$ to a finset is equal to the finite union over the finite set obtained from $s$ of the finite sets obtained from $t(a)$ for each $a \in s$. In symbols: $$ \text{toFinset}(s \mathbin{\text{bind}} t) = \bigcup_{a \in \text{toFinset}(s)} \text{toFinset}(t(a)) $$

Finset.biUnion_mono theorem

(h : ∀ a ∈ s, t₁ a ⊆ t₂ a) : s.biUnion t₁ ⊆ s.biUnion t₂

Full source

lemma biUnion_mono (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) : s.biUnion t₁ ⊆ s.biUnion t₂ := by
  have : ∀ b a, a ∈ s → b ∈ t₁ a → ∃ a : α, a ∈ s ∧ b ∈ t₂ a := fun b a ha hb ↦
    ⟨a, ha, Finset.mem_of_subset (h a ha) hb⟩
  simpa only [subset_iff, mem_biUnion, exists_imp, and_imp, exists_prop]

Monotonicity of Finite Union with Respect to Subset Inclusion

Informal description

For any finite set $s$ of type $\alpha$ and functions $t_1, t_2 : \alpha \to \text{Finset} \beta$, if for every $a \in s$ we have $t_1(a) \subseteq t_2(a)$, then the finite union $\bigcup_{a \in s} t_1(a)$ is a subset of the finite union $\bigcup_{a \in s} t_2(a)$.

Finset.biUnion_subset_biUnion_of_subset_left theorem

(t : α → Finset β) (h : s₁ ⊆ s₂) : s₁.biUnion t ⊆ s₂.biUnion t

Full source

lemma biUnion_subset_biUnion_of_subset_left (t : α → Finset β) (h : s₁ ⊆ s₂) :
    s₁.biUnion t ⊆ s₂.biUnion t := fun x ↦ by
  simp only [and_imp, mem_biUnion, exists_prop]; exact Exists.imp fun a ha ↦ ⟨h ha.1, ha.2⟩

Monotonicity of Finite Union with Respect to Subset Inclusion

Informal description

For any function $t : \alpha \to \text{Finset} \beta$ and finite sets $s_1, s_2 \subseteq \alpha$, if $s_1 \subseteq s_2$, then the finite union $\bigcup_{a \in s_1} t(a)$ is a subset of the finite union $\bigcup_{a \in s_2} t(a)$.

Finset.subset_biUnion_of_mem theorem

(u : α → Finset β) {x : α} (xs : x ∈ s) : u x ⊆ s.biUnion u

Full source

lemma subset_biUnion_of_mem (u : α → Finset β) {x : α} (xs : x ∈ s) : u x ⊆ s.biUnion u :=
  singleton_biUnion.superset.trans <|
    biUnion_subset_biUnion_of_subset_left u <| singleton_subset_iff.2 xs

Inclusion of Function Image in Finite Union: $u(x) \subseteq \bigcup_{a \in s} u(a)$ for $x \in s$

Informal description

For any function $u : \alpha \to \text{Finset} \beta$ and any element $x \in \alpha$ such that $x$ is in the finite set $s$, the finite set $u(x)$ is a subset of the finite union $\bigcup_{a \in s} u(a)$.

Finset.biUnion_subset_iff_forall_subset theorem

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

Full source

@[simp]
lemma biUnion_subset_iff_forall_subset {α β : Type*} [DecidableEq β] {s : Finset α}
    {t : Finset β} {f : α → Finset β} : s.biUnion f ⊆ ts.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t :=
  ⟨fun h _ hx ↦ (subset_biUnion_of_mem f hx).trans h, fun h _ hx ↦
    let ⟨_, ha₁, ha₂⟩ := mem_biUnion.mp hx
    h _ ha₁ ha₂⟩

Finite Union Subset Criterion: $\bigcup_{x \in s} f(x) \subseteq t \leftrightarrow \forall x \in s, f(x) \subseteq t$

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any function $f : \alpha \to \text{Finset} \beta$, the finite union $\bigcup_{x \in s} f(x)$ is a subset of $t$ if and only if for every $x \in s$, the finite set $f(x)$ is a subset of $t$. In symbols: \[ \bigcup_{x \in s} f(x) \subseteq t \leftrightarrow \forall x \in s, f(x) \subseteq t. \]

Finset.biUnion_singleton_eq_self theorem

[DecidableEq α] : s.biUnion (singleton : α → Finset α) = s

Full source

@[simp]
lemma biUnion_singleton_eq_self [DecidableEq α] : s.biUnion (singleton : α → Finset α) = s :=
  ext fun x ↦ by simp only [mem_biUnion, mem_singleton, exists_prop, exists_eq_right']

Union of Singletons Equals Original Set

Informal description

For any finite set $s$ of type $\alpha$ with decidable equality, the union of the singleton sets $\{a\}$ for all $a \in s$ is equal to $s$ itself, i.e., $\bigcup_{a \in s} \{a\} = s$.

Finset.filter_biUnion theorem

 (s : Finset α) (f : α → Finset β) (p : β → Prop) [DecidablePred p] :
  (s.biUnion f).filter p = s.biUnion fun a ↦ (f a).filter p

Full source

lemma filter_biUnion (s : Finset α) (f : α → Finset β) (p : β → Prop) [DecidablePred p] :
    (s.biUnion f).filter p = s.biUnion fun a ↦ (f a).filter p := by
  ext b
  simp only [mem_biUnion, exists_prop, mem_filter]
  constructor
  · rintro ⟨⟨a, ha, hba⟩, hb⟩
    exact ⟨a, ha, hba, hb⟩
  · rintro ⟨a, ha, hba, hb⟩
    exact ⟨⟨a, ha, hba⟩, hb⟩

Filtering Commutes with Finite Union: $\left(\bigcup_{a \in s} f(a)\right) \cap p = \bigcup_{a \in s} (f(a) \cap p)$

Informal description

Let $s$ be a finite set of type $\alpha$, $f : \alpha \to \text{Finset} \beta$ a function mapping each element of $\alpha$ to a finite set of type $\beta$, and $p : \beta \to \text{Prop}$ a decidable predicate on $\beta$. Then the finite set obtained by first taking the union $\bigcup_{a \in s} f(a)$ and then filtering by $p$ is equal to the union of the finite sets obtained by filtering each $f(a)$ by $p$ for $a \in s$. In symbols: \[ \left(\bigcup_{a \in s} f(a)\right) \cap \{b \mid p(b)\} = \bigcup_{a \in s} \left(f(a) \cap \{b \mid p(b)\}\right). \]

Finset.biUnion_filter_eq_of_maps_to theorem

 [DecidableEq α] {s : Finset α} {t : Finset β} {f : α → β} (h : ∀ x ∈ s, f x ∈ t) :
  (t.biUnion fun a ↦ s.filter fun c ↦ f c = a) = s

Full source

lemma biUnion_filter_eq_of_maps_to [DecidableEq α] {s : Finset α} {t : Finset β} {f : α → β}
    (h : ∀ x ∈ s, f x ∈ t) : (t.biUnion fun a ↦ s.filter fun c ↦ f c = a) = s := by
  simpa only [disjiUnion_eq_biUnion] using disjiUnion_filter_eq_of_maps_to h

Union of Fibers Equals Original Set Under Mapping Condition

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$ (with decidable equality on $\alpha$), and any function $f \colon \alpha \to \beta$ such that $f(x) \in t$ for all $x \in s$, the union over $a \in t$ of the sets $\{x \in s \mid f(x) = a\}$ equals $s$. In symbols: \[ \bigcup_{a \in t} \{x \in s \mid f(x) = a\} = s \]

Finset.erase_biUnion theorem

(f : α → Finset β) (s : Finset α) (b : β) : (s.biUnion f).erase b = s.biUnion fun x ↦ (f x).erase b

Full source

lemma erase_biUnion (f : α → Finset β) (s : Finset α) (b : β) :
    (s.biUnion f).erase b = s.biUnion fun x ↦ (f x).erase b := by
  ext a
  simp only [mem_biUnion, not_exists, not_and, mem_erase, ne_eq]
  tauto

Erasing an element commutes with finite unions of finite sets

Informal description

For any function $f : \alpha \to \text{Finset} \beta$, a finite set $s \subseteq \alpha$, and an element $b \in \beta$, the following equality holds: $$ \left(\bigcup_{x \in s} f(x)\right) \setminus \{b\} = \bigcup_{x \in s} \left(f(x) \setminus \{b\}\right) $$ where $\setminus$ denotes set difference and $\bigcup$ denotes the finite union of sets.

Finset.biUnion_nonempty theorem

: (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty

Full source

@[simp]
lemma biUnion_nonempty : (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty := by
  simp only [Finset.Nonempty, mem_biUnion]
  rw [exists_swap]
  simp [exists_and_left]

Nonemptiness of Finite Union of Finite Sets

Informal description

For a finite set $s$ of type $\alpha$ and a function $t : \alpha \to \text{Finset} \beta$, the union $\bigcup_{x \in s} t(x)$ is nonempty if and only if there exists an element $x \in s$ such that $t(x)$ is nonempty. In other words: $$\left(\bigcup_{x \in s} t(x) \neq \emptyset\right) \leftrightarrow \exists x \in s,\ t(x) \neq \emptyset$$

Finset.Nonempty.biUnion theorem

(hs : s.Nonempty) (ht : ∀ x ∈ s, (t x).Nonempty) : (s.biUnion t).Nonempty

Full source

lemma Nonempty.biUnion (hs : s.Nonempty) (ht : ∀ x ∈ s, (t x).Nonempty) :
    (s.biUnion t).Nonempty := biUnion_nonempty.2 <| hs.imp fun x hx ↦ ⟨hx, ht x hx⟩

Nonempty Union of Nonempty Finite Sets

Informal description

For a nonempty finite set $s$ of type $\alpha$ and a function $t : \alpha \to \text{Finset} \beta$, if for every $x \in s$ the finite set $t(x)$ is nonempty, then the finite union $\bigcup_{x \in s} t(x)$ is also nonempty.

Finset.disjoint_biUnion_left theorem

(s : Finset α) (f : α → Finset β) (t : Finset β) : Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

Full source

lemma disjoint_biUnion_left (s : Finset α) (f : α → Finset β) (t : Finset β) :
    DisjointDisjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t := by
  classical
  refine s.induction ?_ ?_
  · simp only [forall_mem_empty_iff, biUnion_empty, disjoint_empty_left]
  · intro i s his ih
    simp only [disjoint_union_left, biUnion_insert, his, forall_mem_insert, ih]

Disjointness of Finite Union with a Set: $\bigcup_{i \in s} f(i) \cap t = \emptyset \leftrightarrow \forall i \in s, f(i) \cap t = \emptyset$

Informal description

For any finite set $s$ of type $\alpha$, any function $f : \alpha \to \text{Finset} \beta$, and any finite set $t$ of type $\beta$, the union $\bigcup_{i \in s} f(i)$ is disjoint from $t$ if and only if for every $i \in s$, the set $f(i)$ is disjoint from $t$. In other words: \[ \bigcup_{i \in s} f(i) \cap t = \emptyset \leftrightarrow \forall i \in s, f(i) \cap t = \emptyset. \]

Finset.disjoint_biUnion_right theorem

(s : Finset β) (t : Finset α) (f : α → Finset β) : Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)

Full source

lemma disjoint_biUnion_right (s : Finset β) (t : Finset α) (f : α → Finset β) :
    DisjointDisjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i) := by
  simpa only [_root_.disjoint_comm] using disjoint_biUnion_left t f s

Disjointness of a Set with a Finite Union: $s \cap \bigcup_{i \in t} f(i) = \emptyset \leftrightarrow \forall i \in t, s \cap f(i) = \emptyset$

Informal description

For any finite set $s$ of type $\beta$, any finite set $t$ of type $\alpha$, and any function $f : \alpha \to \text{Finset} \beta$, the set $s$ is disjoint from the finite union $\bigcup_{i \in t} f(i)$ if and only if for every $i \in t$, the set $s$ is disjoint from $f(i)$. In other words: \[ s \cap \left( \bigcup_{i \in t} f(i) \right) = \emptyset \leftrightarrow \forall i \in t, s \cap f(i) = \emptyset. \]

Finset.image_biUnion theorem

 [DecidableEq γ] {f : α → β} {s : Finset α} {t : β → Finset γ} : (s.image f).biUnion t = s.biUnion fun a => t (f a)

Full source

theorem image_biUnion [DecidableEq γ] {f : α → β} {s : Finset α} {t : β → Finset γ} :
    (s.image f).biUnion t = s.biUnion fun a => t (f a) :=
  haveI := Classical.decEq α
  Finset.induction_on s rfl fun a s _ ih => by simp only [image_insert, biUnion_insert, ih]

Image Union Equals Union of Compositions for Finite Sets: $\bigcup_{b \in f(s)} t(b) = \bigcup_{a \in s} t(f(a))$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types with decidable equality on $\gamma$. For any finite set $s \subseteq \alpha$, any function $f : \alpha \to \beta$, and any function $t : \beta \to \text{Finset} \gamma$, the finite union of $t$ over the image of $s$ under $f$ is equal to the finite union of the composition $t \circ f$ over $s$. That is, \[ \bigcup_{b \in f(s)} t(b) = \bigcup_{a \in s} t(f(a)). \]

Finset.biUnion_image theorem

 [DecidableEq γ] {s : Finset α} {t : α → Finset β} {f : β → γ} :
  (s.biUnion t).image f = s.biUnion fun a => (t a).image f

Full source

theorem biUnion_image [DecidableEq γ] {s : Finset α} {t : α → Finset β} {f : β → γ} :
    (s.biUnion t).image f = s.biUnion fun a => (t a).image f :=
  haveI := Classical.decEq α
  Finset.induction_on s rfl fun a s _ ih => by simp only [biUnion_insert, image_union, ih]

Image of Union Equals Union of Images for Finite Sets under a Function

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types with decidable equality on $\gamma$. For any finite set $s \subseteq \alpha$, any function $t : \alpha \to \text{Finset} \beta$, and any function $f : \beta \to \gamma$, the image of the finite union $\bigcup_{a \in s} t(a)$ under $f$ is equal to the finite union of the images of $t(a)$ under $f$ for all $a \in s$. That is, \[ f\left(\bigcup_{a \in s} t(a)\right) = \bigcup_{a \in s} f(t(a)). \]

Finset.image_biUnion_filter_eq theorem

[DecidableEq α] (s : Finset β) (g : β → α) : ((s.image g).biUnion fun a => s.filter fun c => g c = a) = s

Full source

theorem image_biUnion_filter_eq [DecidableEq α] (s : Finset β) (g : β → α) :
    ((s.image g).biUnion fun a => s.filter fun c => g c = a) = s :=
  biUnion_filter_eq_of_maps_to fun _ => mem_image_of_mem g

Union of Fibers over Image Equals Original Set

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality on $\alpha$. For any finite set $s \subseteq \beta$ and any function $g : \beta \to \alpha$, the union over $a \in g(s)$ of the sets $\{c \in s \mid g(c) = a\}$ equals $s$. In symbols: \[ \bigcup_{a \in g(s)} \{c \in s \mid g(c) = a\} = s \]

Finset.biUnion_singleton theorem

{f : α → β} : (s.biUnion fun a => {f a}) = s.image f

Full source

theorem biUnion_singleton {f : α → β} : (s.biUnion fun a => {f a}) = s.image f :=
  ext fun x => by simp only [mem_biUnion, mem_image, mem_singleton, eq_comm]

Union of Singletons Equals Image of Set

Informal description

For any function $f : \alpha \to \beta$ and finite set $s$ of type $\alpha$, the finite union of singleton sets $\{f(a)\}$ over all $a \in s$ is equal to the image of $s$ under $f$. In other words: \[ \bigcup_{a \in s} \{f(a)\} = f(s) \]

Mathlib.Data.Finset.Union

Main declarations

TODO