Finset.biUnion_mono
theorem Finset.biUnion_mono :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t₁ t₂ : α → Finset β} [inst : DecidableEq β],
(∀ a ∈ s, t₁ a ⊆ t₂ a) → s.biUnion t₁ ⊆ s.biUnion t₂
The theorem `Finset.biUnion_mono` asserts that for any types `α` and `β`, any finite set `s` of `α`, and any two functions `t₁` and `t₂` from `α` to finite sets of `β` (assuming `β` has decidable equality), if for every element `a` in `s`, the finite set `t₁ a` is a subset of `t₂ a`, then the union of `t₁ a` over all `a` in `s` is a subset of the union of `t₂ a` over all `a` in `s`. In other words, if each individual finite set mapped by `t₁` from `s` is contained in the corresponding finite set mapped by `t₂`, then this containment relation is preserved when taking the unions over all elements of `s`.
More concisely: If `β` has decidable equality and for all `a` in a finite set `s`, `t₁ a` is a subset of `t₂ a`, then the union of `t₁ a` over `a` in `s` is a subset of the union of `t₂ a` over `a` in `s`.
|
Finset.mem_biUnion
theorem Finset.mem_biUnion :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β] {b : β},
b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a
The theorem `Finset.mem_biUnion` states that for any types `α` and `β`, a given `Finset` `s` of type `α`, a function `t` mapping from type `α` to `Finset` of type `β` where `β` has decidable equality, and an element `b` of type `β`, `b` is in the biUnion of `s` and `t` if and only if there exists an element `a` in `s` such that `b` is in `t a`. In other words, an element is in the biUnion of a set and a function if it is in the image of the function at some point in the set.
More concisely: For any types `α` and `β` with decidable equality, and a Finset `s` of type `α` and a function `t : α → Finset β`, an element `b` is in the biUnion of `s` and `t` if and only if there exists an `a` in `s` such that `b` is in `t a`.
|
Finset.biUnion_subset
theorem Finset.biUnion_subset :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β] {s' : Finset β},
s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'
The theorem `Finset.biUnion_subset` states that for any types `α` and `β`, a finite set `s` of type `α`, a function `t` mapping elements of type `α` to finite sets of type `β`, and a finite set `s'` of type `β` (with decidable equality), the bi-union of the finite set `s` and the function `t` (represented as `Finset.biUnion s t`) 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, this theorem expresses a condition for a bi-union of a finite set and a function mapping elements to finite sets to be a subset of another finite set.
More concisely: For any finite sets `s` of type `α` and `s'` of type `β` with decidable equality, and a function `t : α → Finset β`, the bi-union `Finset.biUnion s t` is a subset of `s'` if and only if for all `x` in `s`, `t x` is a subset of `s'`.
|
Finset.subset_biUnion_of_mem
theorem Finset.subset_biUnion_of_mem :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} [inst : DecidableEq β] (u : α → Finset β) {x : α},
x ∈ s → u x ⊆ s.biUnion u
The theorem `Finset.subset_biUnion_of_mem` asserts that for any types `α` and `β`, given a finset `s` of type `α`, a function `u` mapping elements of `α` to finsets of `β`, and any element `x` of `α`, if `x` is an element of `s`, then the finset `u(x)` is a subset of the biUnion of `s` and `u`, where the biUnion of `s` and `u` is defined as the union of `u(a)` for all `a` in `s`. This theorem assumes that equality for type `β` is decidable.
More concisely: For any types `α` and `β`, if `s` is a finset of `α`, `u` maps elements of `α` to finsets of `β`, and `x` is an element of `s`, then `u(x)` is a subset of the union of `s` and the image of `u`: `u(x) ⊆ s ∪ {a ∣ a ∈ s} → u a`.
|
Finset.biUnion_insert
theorem Finset.biUnion_insert :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β] [inst_1 : DecidableEq α]
{a : α}, (insert a s).biUnion t = t a ∪ s.biUnion t
The theorem `Finset.biUnion_insert` states that for any types `α` and `β`, any finite set `s` of type `α`, any function `t : α → Finset β` that maps elements of `α` to finite sets of `β`, any element `a : α`, and provided that both `α` and `β` have decidable equality, the biUnion of the function `t` over the set obtained by inserting `a` into `s` is equal to the union of `t` applied to `a` and the biUnion of `t` over `s`. In mathematical terms, it means that for all `a ∈ α` and `s ⊆ α`, we have that `⋃_{x ∈ (a ∪ s)} t(x) = t(a) ∪ ⋃_{x ∈ s} t(x)`. Thus, it expresses a property of the biUnion operation analogous to the distributive law of union over insert in set theory.
More concisely: For any types `α` and `β` with decidable equality, and given a finite set `s` of type `α` and a function `t : α → Finset β`, the biUnion of `t` over `a ∪ s` equals the union of `t(a)` and the biUnion of `t` over `s`, for all `α` elements `a`.
|
Finset.disjiUnion_eq_biUnion
theorem Finset.disjiUnion_eq_biUnion :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset α) (f : α → Finset β)
(hf : (↑s).PairwiseDisjoint f), s.disjiUnion f hf = s.biUnion f
The theorem `Finset.disjiUnion_eq_biUnion` states that for any finite set `s` of type `α` and any function `f` from `α` to finite sets of type `β` (where `β` has decidable equality), if the sets resulting from applying `f` to distinct elements of `s` are pairwise disjoint, then the disjoint union of these sets as defined by `Finset.disjiUnion` is equal to the union of these sets as defined by `Finset.biUnion`. In other words, when the sets are guaranteed to be disjoint, the two methods of forming a union give the same result.
More concisely: For any finite set `s` and function `f` from a set `α` to finite sets of `β` with decidable equality, if the sets `f x` and `f y` are disjoint for distinct `x` and `y` in `s`, then `Finset.disjiUnion (map f s) = Finset.biUnion (map f ``s``)`.
|
Finset.coe_biUnion
theorem Finset.coe_biUnion :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β],
↑(s.biUnion t) = ⋃ x ∈ ↑s, ↑(t x)
The theorem `Finset.coe_biUnion` states that for any two types `α` and `β`, a finite set `s` of type `α`, and a function `t` mapping elements of `α` to a finite set of `β`, given that `β` has decidable equality, the set of elements generated by taking the union of `t a` for each `a` in `s` (represented as `Finset.biUnion s t`), when converted to a set, is equal to the union of sets `t x` for each `x` in the set converted from `s`. In mathematical notation, it says that the set of `Finset.biUnion s t` is equivalent to the union of the sets `t x` for all `x` in the set `s`, i.e., $↑(Finset.biUnion\ s\ t) = ⋃_{x ∈ ↑s} ↑(t\ x)$.
More concisely: For any finite set $s$ and function $t$, if $\beta$ has decidable equality, then $↑(Finset.biUnion\ s\ t) = ⋃_{x \in s} ↑(t\ x)$.
|