Set.biUnion_eq_iUnion
theorem Set.biUnion_eq_iUnion :
∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x ∈ s → Set β),
⋃ x, ⋃ (h : x ∈ s), t x h = ⋃ x, t ↑x ⋯
This theorem states that for any type `α` and `β`, given a set `s` of type `α` and a function `t` that for each element `x` in the set `s` associates a set of type `β`, the union over all `x` of the unions over all proofs `h` that `x` is in `s` of the set `t x h` is equal to the union over all `x` of the set `t ↑x`. In simpler terms, it shows that the union of all subsets defined by a membership-dependent function over a set is the same as the union of subsets when we consider each element in that set, which is a property about how sets can be unionized in Lean 4.
More concisely: For any type `α` and `β`, given a set `s` of type `α` and a function `t : s → Set β`, the union over all `x ∈ s` of the sets `t x <| mem s x` is equal to the set `{y | ∃ x ∈ s, y ∈ t x}`.
|
Set.iInter_subset_of_subset
theorem Set.iInter_subset_of_subset :
∀ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} {t : Set α} (i : ι), s i ⊆ t → ⋂ i, s i ⊆ t
This theorem, `Set.iInter_subset_of_subset`, states that for any type `α`, index type `ι`, function `s` mapping from `ι` to a set of `α`, and a set `t` of `α`, if a specific set `s i` (for some `i` of type `ι`) is a subset of `t`, then the intersection over all `s i` (denoted by `⋂ i, s i`) is also a subset of `t`. In simpler terms, if a specific set from a collection of sets is contained within another set, then the intersection of all sets in that collection is also contained within the latter set.
More concisely: If for all i in ι, si ⊆ t, then ⋂ i, si ⊆ t. (In other words, if every si is a subset of t, then the intersection of all si is a subset of t.)
|
Set.union_iUnion
theorem Set.union_iUnion :
∀ {β : Type u_2} {ι : Sort u_4} [inst : Nonempty ι] (s : Set β) (t : ι → Set β), s ∪ ⋃ i, t i = ⋃ i, s ∪ t i := by
sorry
This theorem states that for any type `β`, any indexed type `ι`, given that `ι` is nonempty, and any set `s` of type `β` and a function `t` from `ι` to sets of `β`, the union of `s` and the indexed union over all `t i` (for all `i` in `ι`) is equal to the indexed union over the union of `s` and `t i`. In mathematical terms, it's stating that $s \cup (\bigcup_{i} t_i) = \bigcup_{i} (s \cup t_i)$. This is a generalization of the distributive law for unions in set theory.
More concisely: For any type `β` and nonempty indexed type `ι`, given sets `s` of type `β` and a function `t` from `ι` to sets of `β`, the indexed union of `s` with `t i` for all `i` in `ι` is equal to the union of `s` with the union of all `t i`. That is, $\bigcup\_i (s \cup t\_i) = s \cup (\bigcup\_i t\_i)$.
|
Set.image2_iUnion₂_right
theorem Set.image2_iUnion₂_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} (f : α → β → γ) (s : Set α)
(t : (i : ι) → κ i → Set β), Set.image2 f s (⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, Set.image2 f s (t i j)
This theorem states that for any types `α`, `β`, and `γ`, and any function `f` from `α` and `β` to `γ`, and any set `s` of type `α`, and a double indexed family of sets `t` of type `β`, the image under `f` of `s` and the union over both indices of `t` is equal to the union over both indices of the image under `f` of `s` and `t`. In other words, applying a function to the elements of a set and a union of sets gives the same result as taking the union of applying the function to the elements of the set and each individual set. This theorem can be described in mathematical notation as: `f(s, ⋃(i,j), t(i,j)) = ⋃(i,j), f(s, t(i,j))`.
More concisely: For any functions `f` from types `α` and `β` to `γ`, sets `s` of type `α`, and double indexed families of sets `t` of type `β`, `f(s ∪ ⋃i,j t(i,j)) = ∪i,j (f(s) ∪ t(i,j))`.
|
Set.sUnion_subset
theorem Set.sUnion_subset : ∀ {α : Type u_1} {S : Set (Set α)} {t : Set α}, (∀ t' ∈ S, t' ⊆ t) → S.sUnion ⊆ t := by
sorry
The theorem `Set.sUnion_subset` states that for any type `α`, and for any set `S` of sets of `α` and any set `t` of `α`, if every set `t'` in `S` is a subset of `t`, then the union over all sets in `S` is also a subset of `t`. This is a theorem that says, intuitively, if `t` contains all the elements of every set in `S`, then `t` contains all the elements in the "big" set that is formed by taking the union of all the sets in `S`.
More concisely: If every set in a family `S` of subsets of type `α` is a subset of a set `t` of `α`, then the union of all sets in `S` is a subset of `t`.
|
Set.mem_sUnion_of_mem
theorem Set.mem_sUnion_of_mem : ∀ {α : Type u_1} {x : α} {t : Set α} {S : Set (Set α)}, x ∈ t → t ∈ S → x ∈ S.sUnion
The theorem `Set.mem_sUnion_of_mem` states that for any type `α`, any element `x` of type `α`, and any two sets `t` and `S` of type `α` and set of sets of type `α` respectively, if `x` is an element of `t` and `t` is an element of `S`, then `x` is an element of the union of sets in `S`. In mathematical notation, this can be written as: if $x \in t$ and $t \in S$, then $x \in \bigcup S$. This theorem is essentially stating a property of unions of sets: an element belongs to the union of a collection of sets if and only if it belongs to at least one of the sets in the collection.
More concisely: If a set `t` contains an element `x` and `t` is an element of a set `S` of sets, then `x` is in the union of sets in `S`. In mathematical notation: `x ∈ t` and `t ∈ S` imply `x ∈ ⋃ S`.
|
Set.compl_iInter₂
theorem Set.compl_iInter₂ :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} (s : (i : ι) → κ i → Set α),
(⋂ i, ⋂ j, s i j)ᶜ = ⋃ i, ⋃ j, (s i j)ᶜ
This theorem states that for any type `α` and any two indexed collections of sets `(s i j)` indexed by `ι` and `κ i` respectively, the complement of the intersection over all `i` and `j` of the sets `(s i j)` is equal to the union over all `i` and `j` of the complements of the sets `(s i j)`. In mathematical terms, this corresponds to the statement that the complement of an intersection is equal to the union of the complements, generalized to two levels of indexing.
More concisely: For any indexed collections of sets (s i j) indexed by ι and κ i, the complement of their intersection is equal to the union of the complements of each set (s i j). Mathematically, �� /******/ᶜ i, j. ∣s i j∣∥ = ∱/_i. ∣s i j∣∣'.
This statement can be read as "the complement of the intersection of all sets s i j with respect to their common index i, for all index j, is equal to the union of the complements of all sets s i j with respect to their individual index i."
|
Set.biInter_and'
theorem Set.biInter_and' :
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (p : ι' → Prop) (q : ι → ι' → Prop)
(s : (x : ι) → (y : ι') → p y ∧ q x y → Set α),
⋂ x, ⋂ y, ⋂ (h : p y ∧ q x y), s x y h = ⋂ y, ⋂ (hy : p y), ⋂ x, ⋂ (hx : q x y), s x y ⋯
This theorem, named `Set.biInter_and'`, states that for any type `α`, sorts `ι` and `ι'`, a property `p` of elements from `ι'`, a binary relation `q` between elements from `ι` and `ι'`, and a function `s` that maps an element of `ι`, an element of `ι'`, and a proof that `p y` and `q x y` hold to a set of `α`, the intersection of sets produced by `s` over all `x`, `y`, and proofs of `p y` and `q x y` is equal to the intersection of sets over all `y`, proofs of `p y`, `x`, and proofs of `q x y`.
In simpler terms, this theorem is about the reordering of nested intersections of sets. It says that you can reorder the intersections without changing the resulting set, when dealing with a particular kind of function `s` that produces sets from elements of `ι` and `ι'` and proofs of certain properties.
More concisely: For any type `α`, sets `ι` and `ι'`, property `p` of elements from `ι'`, binary relation `q` between elements from `ι` and `ι'`, and function `s` that maps an element of `ι`, an element of `ι'`, and proofs of `p y` and `q x y` to sets of `α`, the sets `∩����'_x (s x) (∀ y, p y) (∀ y, q x y)` and `∩����'_y (∀ x, ∀ y, s x y) (p y)` are equal.
|
Set.inter_iInter
theorem Set.inter_iInter :
∀ {β : Type u_2} {ι : Sort u_4} [inst : Nonempty ι] (s : Set β) (t : ι → Set β), s ∩ ⋂ i, t i = ⋂ i, s ∩ t i := by
sorry
This theorem states that for any type `β` and any indexed type `ι` (where `ι` is nonempty), given a set `s` of `β` and a function `t` that maps from `ι` to a set of `β`, the intersection of set `s` with the intersection of all sets `t i` (where `i` ranges over `ι`) is equal to the intersection, over all `i`, of set `s` and the individual sets `t i`. In terms of set theory, this is expressing a distributive property of intersections, namely that the intersection of a set with the intersection of a family of sets can be computed by taking the intersection, for each set in the family, of the set with that set. In mathematical notation, this is saying that `s ∩ (∩i, t i) = ∩i, s ∩ t i`.
More concisely: The theorem asserts that for any set `s` and a family of sets `{ti : ι | i ∈ ι}`, the intersection of `s` with the intersection of all `ti` is equal to the intersection of `s` with each `ti` over all `i` in `ι`. In symbols: `s ∩ (∧i, ti) = ∧i, s ∩ ti`.
|
Set.iInter_of_empty
theorem Set.iInter_of_empty : ∀ {α : Type u_1} {ι : Sort u_4} [inst : IsEmpty ι] (s : ι → Set α), ⋂ i, s i = Set.univ
The theorem `Set.iInter_of_empty` states that for any type `α` and an `ι` sort (an index set) such that `ι` is empty, any function `s` from `ι` to `Set α` (mapping indices to sets of `α`), the intersection of all sets `s i` (for `i` in `ι`) is the universal set `Set.univ`. In other words, if we have no sets to intersect (because `ι` is empty), then the intersection is the universal set, which includes all possible elements of type `α`.
More concisely: For any empty index set `ι` and any function `s` from `ι` to sets of type `α`, the intersection of all sets `s i` is the universal set `Set.univ` of type `Set α`.
|
Set.sUnion_mem_empty_univ
theorem Set.sUnion_mem_empty_univ : ∀ {α : Type u_1} {S : Set (Set α)}, S ⊆ {∅, Set.univ} → S.sUnion ∈ {∅, Set.univ}
The theorem `Set.sUnion_mem_empty_univ` states that for any type `α` and any set `S` of sets of `α`, if all the sets in `S` are either the empty set `∅` or the universal set (i.e., the set of all elements of `α`), then the union of all the sets in `S` is also either `∅` or the universal set. In other words, if we have a collection of sets where each individual set contains either no elements or all possible elements of a certain type, then when we combine all these sets together, the resulting set will also contain either no elements or all possible elements of the same type.
More concisely: If every set in a collection of sets over type `α` is either the empty set or the universal set, then their union is also the empty set or the universal set.
|
Set.iUnion_prod'
theorem Set.iUnion_prod' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β × γ → Set α), ⋃ x, f x = ⋃ i, ⋃ j, f (i, j)
This theorem states that for any types `α`, `β`, and `γ`, and any function `f` mapping pairs of elements from `β` and `γ` to sets of `α`, the union over all pairs `(i, j)` of the sets `f(i, j)` is equal to the union over all `x` of the sets `f(x)`. In other words, the union taken over all pairs is the same as the union taken over all points in the Cartesian product.
More concisely: For any function `f` mapping pairs from `β x γ` to sets of `α`, the union of `{f (i, j) | (i, j) ∈ β x γ}` equals the union of `{f x | x ∈ β x γ}`.
|
Set.image2_iInter₂_subset_right
theorem Set.image2_iInter₂_subset_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} (f : α → β → γ) (s : Set α)
(t : (i : ι) → κ i → Set β), Set.image2 f s (⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, Set.image2 f s (t i j)
The theorem `Set.image2_iInter₂_subset_right` states that for all types `α`, `β`, `γ`, a function `f` from `α` and `β` to `γ`, a set `s` of type `α`, and a dependent family of sets `t` of type `β` indexed by `ι` and `κ`, the image set of `f` with respect to `s` and the intersection of all sets `t i j` is a subset of the intersection of all image sets of `f` with respect to `s` and each `t i j`. In other words, it states that applying a function to elements from a set and an intersection of sets results in a set that is contained within the intersection of the sets resulted from applying the function to elements from the set and each set in the intersection individually.
More concisely: For all types α, β, γ, function f from α × β to γ, set s ∈ α, and dependent family of sets t(ι, κ) ∈ β, the image of s under f and the intersections of t(ι, κ) are included in the intersections of the images of s under f and each t(ι, κ).
|
Set.setOf_exists
theorem Set.setOf_exists : ∀ {β : Type u_2} {ι : Sort u_4} (p : ι → β → Prop), {x | ∃ i, p i x} = ⋃ i, {x | p i x} := by
sorry
This theorem, `Set.setOf_exists`, states that for any type `β` and any abstract sort `ι`, given a predicate `p : ι → β → Prop`, the set of elements `x` that satisfy the property "there exists an `i` such that `p i x` holds" is equal to the union over all `i` of the sets of `x` for which `p i x` holds. Essentially, this theorem expresses that you can interchange the order of quantification and set formation.
More concisely: For any type `β` and abstract sort `ι` with predicate `p : ι → β → Prop`, the set of `x` such that there exists an `i` with `p i x` is equivalent to the union of the sets of `x` satisfying `p i x` for all `i`.
|
Set.compl_iInter
theorem Set.compl_iInter : ∀ {β : Type u_2} {ι : Sort u_4} (s : ι → Set β), (⋂ i, s i)ᶜ = ⋃ i, (s i)ᶜ
The theorem `Set.compl_iInter` states that for all types `β` and any index type `ι`, given a function `s` from `ι` to the set of `β`, the complement of the intersection over `ι` of the sets `s i` is equal to the union of the complements of the sets `s i`. This is an application of De Morgan's laws to sets. In mathematical terms, this can be written as $(\bigcap_{i \in I} s_i)^c = \bigcup_{i \in I} (s_i)^c$, where `I` is an index set, `s_i` is a set for each `i` in `I`, and `^c` denotes the complement of a set.
More concisely: The complement of the intersection of a family of sets indexed by an index type is equal to the union of the complements of the sets in the family. (In mathematical notation: (⋂i∈I si)c = ⋃i∈I sc, where I is an index set, si is a set for each i in I, and ^c denotes the complement of a set.)
|
Mathlib.Data.Set.Lattice._auxLemma.5
theorem Mathlib.Data.Set.Lattice._auxLemma.5 :
∀ {α : Type u_1} {ι : Sort u_4} {s : Set α} {t : ι → Set α}, (s ⊆ ⋂ i, t i) = ∀ (i : ι), s ⊆ t i
This theorem states that for any type `α` and any sort `ι`, and given a set `s` of type `α` and a function `t` mapping `ι` to a set of type `α`, the statement "set `s` is a subset of the intersection of the set `t i` for all `i` belonging to the sort `ι`" is equivalent to "for all `i` in `ι`, set `s` is a subset of the set `t i`". In other words, a set `s` is a subset of the intersection of a family of sets if and only if it is a subset of each set in the family.
More concisely: For any type `α` and sort `ι`, a set `s` of type `α` is equal to the intersection of sets `{t i | i ∈ ι}`, if and only if `s` is a subset of each `t i`.
|
Set.iUnion₂_subset_iff
theorem Set.iUnion₂_subset_iff :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {t : Set α},
⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t
This theorem, `Set.iUnion₂_subset_iff`, states that for all types `α` and `ι`, and for a type family `κ` indexed over `ι`, given a doubly-indexed collection of sets `s` (indexed over both `ι` and `κ i`) and a set `t`, the union over all `i` and `j` of the sets `s i j` is a subset of `t` if and only if for each `i` in `ι` and `j` in `κ i`, the set `s i j` is a subset of `t`. In other words, the union of a collection of sets is within some set `t` precisely when each individual set in the collection is within `t`.
More concisely: For all types `α`, `ι`, and type families `κ`, and for a collection `s` of sets indexed over `ι` and `κ i`, `⋃ₕ i, j in ι × κ i, s i j ⊆ t` if and only if `∀i ∈ ι, ∀j ∈ κ i, s i j ⊆ t`.
|
Set.image2_iUnion_left
theorem Set.image2_iUnion_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : ι → Set α) (t : Set β),
Set.image2 f (⋃ i, s i) t = ⋃ i, Set.image2 f (s i) t
The theorem `Set.image2_iUnion_left` states that for all types α, β, and γ, and all types ι (which can be thought of as an index set), given a binary function `f` from α and β to γ, a function `s` from ι to the set of α, and a set `t` of β, the image under `f` of the union over all `i` of `s i` and `t` is equal to the union over all `i` of the image under `f` of `s i` and `t`. In simple words, applying a function to the union of sets is the same as taking the union of the function applied to each set, essentially proving a property similar to the distributivity of function application over set union for the left side of the function.
More concisely: For all types α, β, γ, index set ι, function f : α × β → γ, set s : ι → α, and set t : Set β, the image of the union of sets s i and t under f is equal to the union of the images of sets si and t under f.
|
Set.sUnion_diff_singleton_empty
theorem Set.sUnion_diff_singleton_empty : ∀ {α : Type u_1} (s : Set (Set α)), (s \ {∅}).sUnion = s.sUnion
This theorem, `Set.sUnion_diff_singleton_empty`, states that for any type `α` and for any collection `s` of sets of type `α`, the union over the collection obtained by removing the empty set from `s` is equal to the union over the original collection `s`. In other words, excluding the empty set from a collection of sets does not change the union of the collection. This theorem can be seen as a property regarding the interaction between set union and set difference operations.
More concisely: For any type `α` and collection `s` of sets of type `α`, the set difference of `s` with the empty set is equal to `s` itself when considering set unions. That is, `⋃(s \ {}) = ⋃s`.
|
Set.mem_iInter₂
theorem Set.mem_iInter₂ :
∀ {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} {x : γ} {s : (i : ι) → κ i → Set γ},
x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j
This theorem states that for any type `γ`, any sort `ι`, any sort-dependent family `κ` indexed by `ι`, any element `x` of type `γ`, and any double-indexed family `s` of sets of elements of type `γ`, the element `x` is in the intersection over all `i` and `j` of the sets `s i j` if and only if, for every `i` of type `ι` and every `j` of type `κ i`, `x` is in `s i j`. In terms of set theory, this means that an element belongs to the intersection of a collection of sets if and only if it belongs to each set in the collection.
More concisely: For any type `γ`, sort `ι`, sort-dependent family `κ`, element `x` of type `γ`, and sets `s i j` indexed by `ι` and `κ i`, `x` is in the intersections of all `s i j` if and only if it is in each `s i j`.
|
Set.monotone_preimage
theorem Set.monotone_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Monotone (Set.preimage f)
The theorem `Set.monotone_preimage` states that for any types `α` and `β` and any function `f` from `α` to `β`, the preimage operation of the function `f` is monotone. In other words, if we have two sets `A` and `B` such that `A` is a subset of `B`, then the preimage of `A` under `f` is also a subset of the preimage of `B` under `f`. This follows from the definition of monotonicity and preimage.
More concisely: For any functions between types, the preimage of a subset under the function is monotone, meaning the preimage of a smaller set is included in the preimage of a larger set.
|
Set.sUnion_empty
theorem Set.sUnion_empty : ∀ {α : Type u_1}, ∅.sUnion = ∅
This theorem states that the set union of an empty set of sets is also an empty set. In other words, given any type `α`, the union over all elements (which are sets themselves) in an empty set of sets results in an empty set. This is an application of the set theory principle that the union of no sets results in no elements.
More concisely: The union of an empty set of sets is an empty set.
|
Set.iInter_univ
theorem Set.iInter_univ : ∀ {α : Type u_1} {ι : Sort u_4}, ⋂ x, Set.univ = Set.univ
The theorem `Set.iInter_univ` states that for any type `α` and for any index set `ι`, the intersection of the universal set over all elements of the index set is still the universal set. In other words, if we take the intersection of the universal set across any collection of indices, we will always end up with the universal set, i.e., the set containing all elements of the type `α`. In formal mathematics notation, this can be written as: ∀α, ι, ⋂ₓ (Set.univ) = Set.univ.
More concisely: The theorem asserts that the intersection of the universe over all indices in any index set is equal to the universe itself for any type `α`.
|
Set.subset_biUnion_of_mem
theorem Set.subset_biUnion_of_mem :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {u : α → Set β} {x : α}, x ∈ s → u x ⊆ ⋃ x ∈ s, u x
This theorem states that for any types `α` and `β`, given a set `s` of elements of type `α`, a function `u` from `α` to a set of `β`, and an element `x` of type `α`, if `x` is in `s`, then the set `u(x)` is a subset of the union over all `x` in `s` of `u(x)`. In mathematical notation, this can be written as: if $x \in s$, then $u(x) \subseteq \bigcup_{x \in s} u(x)$.
More concisely: For any set `s` of type `α`, function `u` from `α` to a set of `β`, and `x` in `α` belonging to `s`, `u(x)` is a subset of the union of `u(y)` over all `y` in `s`.
|
Set.mem_biInter
theorem Set.mem_biInter :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : α → Set β} {y : β}, (∀ x ∈ s, y ∈ t x) → y ∈ ⋂ x ∈ s, t x := by
sorry
The theorem `Set.mem_biInter` states that for any types `α` and `β`, any set `s` of type `α`, any function `t` from `α` to a set of `β`, and any element `y` of type `β`, if `y` is in `t x` for every `x` in the set `s`, then `y` is in the intersection of `t x` over all `x` in `s`. In mathematical terms, it says if $y \in t(x)$ for all $x \in s$, then $y \in \bigcap_{x \in s} t(x)$.
More concisely: If a element `y` is in the image of function `t` for every element `x` in set `s`, then `y` is in the intersection of the images of `t` over all elements in `s`. In mathematical notation, $\forall x \in s, y \in t(x) \implies y \in \bigcap\_{x \in s} t(x)$.
|
Set.iInter_congr_Prop
theorem Set.iInter_congr_Prop :
∀ {α : Type u_1} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q),
(∀ (x : q), f₁ ⋯ = f₂ x) → Set.iInter f₁ = Set.iInter f₂
This theorem states that for any type `α`, and any proposition `p` and `q`, and any functions `f₁` and `f₂` from `p` and `q` respectively to a set of `α`, if `p` is equivalent to `q` (`p ↔ q`), and for all elements `x` of `q` the result of `f₁` applied to some value is equal to `f₂` applied to `x`, then the indexed intersection over `f₁` is equal to the indexed intersection over `f₂`. In other words, if `p` and `q` are logically equivalent and both `f₁` and `f₂` produce the same sets for corresponding inputs, then the intersection of all sets generated by `f₁` and `f₂` are the same.
More concisely: If `p` is equivalent to `q` and for all `x` in `q`, `f₁(x) = f₂(x)`, then the indexed intersections of `f₁` and `f₂` over `α` are equal.
|
Set.subset_sInter
theorem Set.subset_sInter : ∀ {α : Type u_1} {S : Set (Set α)} {t : Set α}, (∀ t' ∈ S, t ⊆ t') → t ⊆ S.sInter := by
sorry
This theorem states that for all types `α`, and for all sets `S` of sets of `α`, and for all sets `t` of `α`, if every set `t'` that is an element of `S` is a superset of `t` (`t` is a subset of `t'`), then `t` is also a subset of the intersection of all sets in `S`. In mathematical terms, if for all `t'` in `S`, `t ⊆ t'`, then `t` is a subset of the intersection (`⋂`) of all the sets in `S`.
More concisely: If every set in a family of sets containing a given set is a superset of it, then the given set is a subset of their intersection.
|
Set.sigmaToiUnion_surjective
theorem Set.sigmaToiUnion_surjective :
∀ {α : Type u_1} {β : Type u_2} (t : α → Set β), Function.Surjective (Set.sigmaToiUnion t)
This theorem states that for any type `α` and `β`, and for any function `t` from `α` to the set of `β`, the function `Set.sigmaToiUnion` with `t` as its argument is always surjective. In other words, every element of the union of sets `t i` for all `i` in `α` is an image of some element from the sigma type `(i : α) × ↑(t i)`. The sigma type aggregates all pairs of an element from `α` and an element from the corresponding set `t i`. The surjectivity implies that each element in the union of all `t i` can be traced back to at least one such pair in the sigma type.
More concisely: For any function `t` from type `α` to sets of type `β`, the function `Set.sigmaToiUnion` of `t` is a surjection from the sigma type `(i : α) × ↑(t i)` to the union of images `t i` for all `i` in `α`.
|
Set.sInter_image
theorem Set.sInter_image :
∀ {α : Type u_1} {β : Type u_2} (f : α → Set β) (s : Set α), (f '' s).sInter = ⋂ x ∈ s, f x
This theorem, `Set.sInter_image`, states that for any types `α` and `β`, for any function `f` from `α` to a set of `β`, and for any set `s` of type `α`, the intersection over the image of `s` under `f` is equal to the intersection over all elements `x` in `s` of the sets `f(x)`. In mathematical notation, this says that if `f : α → P(β)` is a function and `s ⊆ α`, then `⋂₀ (f '' s) = ⋂_{x ∈ s} f(x)`, where `P(β)` denotes the power set of `β`, `f '' s` is the image of `s` under `f`, and `⋂₀` and `⋂_{x ∈ s}` denote intersection over a set and over elements in a set, respectively.
More concisely: For any function `f : α → P(β)` and set `s ⊆ α`, the intersection of the image of `s` under `f` equals the intersection of `f(x)` over all `x ∈ s`. In mathematical notation, `⋂₀ (f '' s) = ⋂_{x ∈ s} f(x)`.
|
Set.sInter_empty
theorem Set.sInter_empty : ∀ {α : Type u_1}, ∅.sInter = Set.univ
This theorem, `Set.sInter_empty`, states that for any type `α`, the intersection over an empty collection of sets is the universal set. In other words, if you have no sets to intersect, you end up with the set containing all possible elements of type `α`. This is analogous to the fact in mathematics that the intersection of an empty family of sets is the universal set.
More concisely: The intersection of an empty family of sets in type `α` is the universe `Set.univ`.
|
Set.InjOn.image_iInter_eq
theorem Set.InjOn.image_iInter_eq :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : Nonempty ι] {s : ι → Set α} {f : α → β},
Set.InjOn f (⋃ i, s i) → f '' ⋂ i, s i = ⋂ i, f '' s i
The theorem `Set.InjOn.image_iInter_eq` states that for any types `α`, `β`, and `ι` (where `ι` is nonempty), a function `f` from `α` to `β`, and a family of sets `s` indexed by `ι`, if the function `f` is injective on the union of all sets in the family `s`, then the image of the intersection of all sets in the family `s` under the function `f` equals to the intersection of the images of each set in the family `s` under the function `f`. This is essentially an extension of the property of injective functions that the image of the intersection of sets is the intersection of their images.
More concisely: If `f: α → β` is injective on the union of a family `{s : ι | s : Set α}`, then `f` maps the intersection of all `s` to the intersection of the images of `s` under `f`.
|
Set.sInter_eq_iInter
theorem Set.sInter_eq_iInter : ∀ {α : Type u_1} {s : Set (Set α)}, s.sInter = ⋂ i, ↑i
This theorem states that, for any type `α` and any set `s` of sets of `α`, the intersection over all elements of `s` (represented as `⋂₀ s` in Lean 4) is equal to the intersection over all elements `i` in `s` (represented as `⋂ i, ↑i`). In other words, this theorem equates two different formulations of the intersection of a collection of sets: one that directly takes the intersection of all sets in the collection, and one that iterates over the collection to compute the intersection.
More concisely: For any type `α` and set `s` of sets of `α`, the intersection of all sets in `s` (⋂ s) is equal to the iterated intersection over each set `i` in `s` (⋂ i, i).
|
Set.mem_iUnion₂
theorem Set.mem_iUnion₂ :
∀ {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} {x : γ} {s : (i : ι) → κ i → Set γ},
x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j
This theorem states that for any type `γ`, any index type `ι`, any dependent type `κ` indexed by `ι`, any element `x` of type `γ`, and any family of sets `s` indexed by `ι` and `κ`, the element `x` belongs to the double union over `ι` and `κ` of the sets `s i j` if and only if there exist indices `i` and `j` such that `x` belongs to the set `s i j`. In other words, an element is in the union of multiple sets if it is in at least one of the sets.
More concisely: Given types `γ`, index type `ι`, a dependent type `κ` indexed by `ι`, an element `x` of type `γ`, and a family of sets `s : ι → κ → Sort_, an element `x` is in the double union `⨄ i, j, s i j` if and only if there exist `i` and `j` such that `x` is in `s i j`.
|
iSup_iUnion
theorem iSup_iUnion :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice β] (s : ι → Set α) (f : α → β),
⨆ a ∈ ⋃ i, s i, f a = ⨆ i, ⨆ a ∈ s i, f a
This theorem, `iSup_iUnion`, states that for all types `α`, `β`, and `ι`, given a complete lattice structure on `β`, a function `s` from `ι` to a set of `α`, and a function `f` from `α` to `β`, the supremum (denoted by `⨆`) of `f a` for any `a` in the union (denoted by `⋃`) of all sets `s i` is equal to the supremum of the suprema of `f a` for `a` in each `s i`. In other words, it asserts the equality between the supreme value obtained through the function `f` applied over a union of sets, and the supreme value obtained through the function `f` applied individually to each set, considering all sets provided by the function `s`.
More concisely: For any complete lattice `β`, function `s` from index set `ι` to sets of type `α`, and function `f` from `α` to `β`, the supremum of `f` applied to the union of `s i` is equal to the supremum of the suprema of `f a` over each `s i`.
|
Set.iUnion_congr_of_surjective
theorem Set.iUnion_congr_of_surjective :
∀ {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂),
Function.Surjective h → (∀ (x : ι), g (h x) = f x) → ⋃ x, f x = ⋃ y, g y
The theorem `Set.iUnion_congr_of_surjective` states that for all types `α`, `ι`, and `ι₂`, and for all functions `f : ι → Set α` and `g : ι₂ → Set α`, and a function `h : ι → ι₂`, if the function `h` is surjective and for all `x : ι`, `g (h x) = f x`, then the indexed union over all `x` in `ι` of the sets `f x` is equal to the indexed union over all `y` in `ι₂` of the sets `g y`. In simpler terms, if we have a surjective function that transforms each element of `ι` into an element of `ι₂` in such a way that the sets these elements index are the same, then the union of all the sets indexed by elements of `ι` is the same as the union of all the sets indexed by elements of `ι₂`.
More concisely: If `h : ι → ι₂` is surjective and for all `x : ι`, `g (h x) = f x`, then `⋃x : ι. f x = ⋃y : ι₂. g y`.
|
Set.biUnion_range
theorem Set.biUnion_range :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → α} {g : α → Set β}, ⋃ x ∈ Set.range f, g x = ⋃ y, g (f y)
This theorem states that for all types `α`, `β`, and `ι`, and for all functions `f : ι → α` and `g : α → Set β`, the union over all elements `x` in the range of `f` of the set `g(x)` is equal to the union over all `y` of the set `g(f(y))`. In other words, it says that the union of the image of the function `g` applied to the range of the function `f` is the same as the union of the image of the function `g` applied to the image of the function `f`. This theorem captures an important property of function composition and union operations in the world of set theory.
More concisely: For all functions `f : ι → α` and `g : α → Set β`, the union of `{g(x) | x ∈ range f}` equals the union of `{g(f(y)) | y ∈ ι}`.
|
Set.biUnion_insert
theorem Set.biUnion_insert :
∀ {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : α → Set β), ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x
The theorem `Set.biUnion_insert` states that for all types `α` and `β`, for any element `a` of type `α`, set `s` which is a collection of elements of type `α`, and a function `t` that maps elements of type `α` to sets of type `β`, the big union of `t x` where `x` belongs to the insertion of `a` into `s`, is equal to the union of `t a` and the big union of `t x` where `x` belongs to `s`. In other words, for any specific element and a set, the big union over the set including that specific element is the same as the union of the specific element and the big union over the rest of the set.
More concisely: For any type `α`, set `s` of `α`, element `a` of `α`, and function `t` mapping `α` to sets of `β`, we have `(⋃ x in s.insert a) t x = t a ∪ (⋃ x in s) t x`.
|
Set.sInter_eq_biInter
theorem Set.sInter_eq_biInter : ∀ {α : Type u_1} {s : Set (Set α)}, s.sInter = ⋂ i ∈ s, i
This theorem states that for any type 'α' and any set 's' of sets of 'α', the intersection of all sets in 's' is equivalent to the intersection of all sets 'i' such that 'i' is an element of 's'. In other words, it means that the intersection over a collection of sets is the same whether it's done as a direct intersection over the collection (notated as ⋂₀ s) or as an intersection over each member of the collection (notated as ⋂ i ∈ s, i).
More concisely: For any type 'α' and set 's' of sets of 'α', the intersection of all sets in 's' is equal to the intersection of all sets 'i' in 's'. In other words, ⋂ i ∈ s, i = ⋂ X ∈ s, X.
|
Set.iUnion_image_right
theorem Set.iUnion_image_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β},
⋃ b ∈ t, (fun x => f x b) '' s = Set.image2 f s t
The theorem `Set.iUnion_image_right` states that for every function `f` from a type `α` to a type `β` to a type `γ`, every set `s` of type `α`, and every set `t` of type `β`, the union of the image of the function `(fun x => f x b)` for each `b` in `t` over the set `s` is equal to the image of the binary function `f` over the sets `s` and `t`. This theorem connects the concept of union and image of functions in the context of sets.
More concisely: For any function `f: α → β`, set `s ∈ Set α`, and set `t ∈ Set β`, the image of `f` over the union of `s` and `t` is equal to the union of the images of `f(x)` for each `x ∈ s` and `f(y)` for each `y ∈ t`.
|
Set.image2_iUnion₂_left
theorem Set.image2_iUnion₂_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} (f : α → β → γ)
(s : (i : ι) → κ i → Set α) (t : Set β), Set.image2 f (⋃ i, ⋃ j, s i j) t = ⋃ i, ⋃ j, Set.image2 f (s i j) t
This theorem states that for any types `α`, `β`, and `γ`, an index type `ι`, and a function `κ` mapping each index to a sort, and given a binary function `f : α → β → γ`, a family of sets `s : (i : ι) → κ i → Set α`, and a set `t : Set β`, the image under `f` of the union over `i` and `j` of the sets `s i j` and `t` is equal to the union, over `i` and `j`, of the image under `f` of `s i j` and `t`. In mathematical terms, this encapsulates the property that the image of a union of sets under a function is the union of the images of those sets, for a family of sets indexed by two indices.
More concisely: For any types `α`, `β`, `γ`, index type `ι`, function `κ : ι -> Sort γ`, binary function `f : α -> β -> γ`, sets `s : ι -> κ i -> Set α`, and set `t : Set β`, we have `unions (map (λ i, map (λ j, f <$> s i <$> j) <*> t) = unions (map (λ i, map (λ j, f <$> s i j) <$> [i, j]))`.
|
Set.iUnion_subset
theorem Set.iUnion_subset :
∀ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} {t : Set α}, (∀ (i : ι), s i ⊆ t) → ⋃ i, s i ⊆ t
This theorem states that for any type `α` and any indexing type `ι`, if you have a family of sets `s` indexed by `ι`, and another set `t` of the same type, then if all sets in the family `s` are subsets of `t`, it follows that the union of all sets in the family `s` is also a subset of `t`. In mathematical terms, given a collection of sets $\{s_i\}_{i \in \iota}$ and a set $t$, if for every $i$ in $\iota$, $s_i \subseteq t$, then $\bigcup_{i} s_i \subseteq t$.
More concisely: If for each index $i$ in $\iota$, set $s\_i$ is a subset of set $t$, then the union of all sets $s\_i$ is also a subset of $t$. (i.e., $\bigcup\_{i \in \iota} s\_i \subseteq t$).
|
Set.subset_iUnion₂
theorem Set.subset_iUnion₂ :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} (i : ι) (j : κ i),
s i j ⊆ ⋃ i', ⋃ j', s i' j'
This theorem is about the relationship between a specific set and the union of a collection of sets. For any type `α`, an index type `ι`, a second index type `κ` dependent on `ι`, and a function `s` that, for each `i` of type `ι` and `j` of type `κ i`, assigns a set of type `α`, the theorem asserts that the set `s i j` is a subset of the union of all sets `s i' j'`, where `i'` ranges over `ι` and `j'` ranges over `κ i'`. In simpler terms, any individual set within a collection of sets is a subset of the union of the entire collection.
More concisely: For any function `s` that assigns to each pair `(i, j)` of indices a set `s i j`, the set `s i j` is a subset of the union of all sets `s i' j'` over all indices `i'` and `j'`.
|
Set.image2_iUnion_right
theorem Set.image2_iUnion_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : Set α) (t : ι → Set β),
Set.image2 f s (⋃ i, t i) = ⋃ i, Set.image2 f s (t i)
The theorem `Set.image2_iUnion_right` states that for all types `α`, `β`, `γ`, and any indexing type `ι`, for any binary function `f` from `α` and `β` to `γ`, any set `s` of type `α`, and any family of sets `t` indexed by `ι` of type `β`, the image under `f` of the set `s` and the union over `ι` of sets `t i` is equal to the union over `i` of the image under `f` of `s` and `t i`. In mathematical terms, this can be expressed as $f(s, \bigcup_i t_i) = \bigcup_i f(s, t_i)$.
More concisely: For any functions $f: \alpha \times \beta \to \gamma$, sets $s:\alpha$, and a family $t: \ι \to \beta$ of sets, $f(s, \bigcup\_{i \in \ι} t\_i) = \bigcup\_{i \in \ι} f(s, t\_i)$.
|
Mathlib.Data.Set.Lattice._auxLemma.2
theorem Mathlib.Data.Set.Lattice._auxLemma.2 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋂ i, s i) = ∀ (i : ι), x ∈ s i
This theorem states that for any type `α`, any sorting type `ι`, any element `x` of type `α`, and any function `s` from `ι` to the set of elements of type `α`, the statement "`x` belongs to the intersection over all `i` of `s i`" is equivalent to "for every `i` in `ι`, `x` belongs to `s i`". In other words, an element is in the intersection of a collection of sets if and only if it is in each set in the collection.
More concisely: For any type `α`, sorting type `ι`, element `x` of type `α`, and function `s` from `ι` to `α`, `x` belongs to the intersection of `s i` for all `i` in `ι` if and only if `x` belongs to every `s i`.
|
Set.biInter_range
theorem Set.biInter_range :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → α} {g : α → Set β}, ⋂ x ∈ Set.range f, g x = ⋂ y, g (f y)
This theorem, `Set.biInter_range`, states that for any types `α`, `β`, and `ι`, and any function `f` from `ι` to `α`, and any function `g` from `α` to a set of `β`, the intersection over `x` in the range of `f` of the sets `g x` equals the intersection over all `y` of the sets `g` applied to `f y`. In other words, it says that when you iterate over all elements in the range of a function and apply another function to them to get a collection of sets, the intersection of these sets is the same as if you just directly applied the second function to each element and took the intersection.
More concisely: For any types `α`, `β`, and `ι`, and functions `f : ι → α` and `g : α → Set β`, the sets `{x ∈ ι | g (f x) ∈ s}` and `{y ∈ Set.range f | g y ∈ s}` have equal intersections for any set `s : Set β`.
|
Set.sInter_range
theorem Set.sInter_range : ∀ {β : Type u_2} {ι : Sort u_4} (f : ι → Set β), (Set.range f).sInter = ⋂ x, f x
This theorem states that for any type `β` and any index set `ι`, for any function `f` from `ι` to the sets of `β`, the intersection over the range of `f` is equal to the intersection for each `x` in `ι` of `f x`. In other words, the set of all elements that belong to every set in the range of `f` is the same as the set of all elements that belong to every set `f x` for each `x` in `ι`.
More concisely: For any function `f` from an index set `ι` to sets of type `β`, the set intersecting over the range of `f` equals the set intersecting each `f x` for `x` in `ι`. In Lean notation: `∩ (range f) = ∏ x in ι, ∩ (f x)`.
|
Set.sUnion_insert
theorem Set.sUnion_insert : ∀ {α : Type u_1} (s : Set α) (T : Set (Set α)), (insert s T).sUnion = s ∪ T.sUnion := by
sorry
This theorem, `Set.sUnion_insert`, states that for any type `α` and any set `s` of type `α`, and another set `T` of sets of type `α`, the union over the set obtained by inserting `s` into `T` is equivalent to the union of `s` and the union over `T`. In terms of set theory, it is equivalent to saying: the union over all the sets in the collection where one additional set `s` is inserted, is the same as the union of that set `s` with the union over the original collection of sets. This theorem is analogous in structure to a fundamental property of unions in set theory.
More concisely: For any type `α` and set `s` of type `α`, and any set `T` of sets of type `α`, the set `s ∪ (⋃ t ∈ T : t)` equals `s ∪ (⋃ t ∈ T : t)`.
|
Set.iUnion_exists
theorem Set.iUnion_exists :
∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {f : Exists p → Set α},
⋃ (x : Exists p), f x = ⋃ i, ⋃ (h : p i), f ⋯
The theorem `Set.iUnion_exists` states that for any type `α` and any indexed type `ι`, given a predicate `p` on `ι` and a function `f` from the existentially quantified predicate `p` to the set of `α`, the union over all sets `f x`, where `x` is an existing `p`, is the same as the union over all elements `i` of the union over all `h` such that `p i` holds of `f h`. In simpler terms, this theorem is about equivalent ways of forming unions of sets, where the sets are generated by a function `f` applied to indices that satisfy a certain property `p`.
More concisely: For any type `α` and indexed type `ι`, if `p` is a predicate on `ι` and `f` is a function from `p` to `α`, then `⋃(x : ι | p x) ≈ ⋃(i : ⋃h, p h) . f h`.
|
Set.iUnion_subset_iff
theorem Set.iUnion_subset_iff :
∀ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} {t : Set α}, ⋃ i, s i ⊆ t ↔ ∀ (i : ι), s i ⊆ t
This theorem, `Set.iUnion_subset_iff`, states that for any type `α`, any indexing type `ι`, any index-dependent family of sets `s` of type `α`, and any set `t` of type `α`, the union (over all indices, denoted by `⋃ i`) of the family of sets `s` is a subset of `t` if and only if for each index `i` in `ι`, the corresponding set `s i` is a subset of `t`. In other words, it establishes the equivalence between the subset relationship of the union of a collection of sets and the individual sets in the collection to a specific set. This theorem is a fundamental principle in set theory.
More concisely: The theorem `Set.iUnion_subset_iff` in Lean 4 states that for any type `α`, indexing type `ι`, family of sets `s i` indexed by `ι`, and set `t` of type `α`, `⋃ i, s i ⊆ t` if and only if `∀ i, s i ⊆ t`. (The union of the family `s` is a subset of `t` if and only if each `s i` is a subset of `t`. )
|
Set.iUnion_subtype
theorem Set.iUnion_subtype :
∀ {α : Type u_1} {β : Type u_2} (p : α → Prop) (s : { x // p x } → Set β),
⋃ x, s x = ⋃ x, ⋃ (hx : p x), s ⟨x, hx⟩
The theorem `Set.iUnion_subtype` states that for any type `α` and `β`, and any property `p` of `α` and a function `s` that maps elements of `α` satisfying `p` to sets of `β`, the union over all `x` of the sets `s` of `x` is equal to the union over all `x`, and for those `x` that satisfy the property `p`, of the sets `s` of `x` with the property `p`. In other words, this theorem expresses the equality of two different ways of forming a union of sets, one in which the sets are indexed by elements satisfying a certain property, and another where the sets are indexed by elements directly, but the union is only taken over elements that satisfy the property.
More concisely: For any type `α`, property `p` of `α`, and function `s : α → Set β`, the union of `{x : α | p x} Map s = (⋃x : α. p x) s x`.
|
Set.iUnion_image_left
theorem Set.iUnion_image_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β},
⋃ a ∈ s, f a '' t = Set.image2 f s t
This theorem states that for any three types `α`, `β`, and `γ`, and for any binary function `f` from `α` and `β` to `γ`, and for any sets `s` of type `α` and `t` of type `β`, the union over all elements `a` in the set `s` of the image under `f` of `t` (where `a` is held fixed and each element of `t` is mapped to `γ`), is equal to the image of the sets `s` and `t` under the binary function `f`. In other words, when we take an element from `s`, apply the function `f` to this element and each element of `t`, and then take the union over all such elements from `s`, we get exactly the set of all results of applying `f` to elements of `s` and `t`.
More concisely: For any sets `s` of type `α` and `t` of type `β`, and any binary function `f` from `α` and `β` to `γ`, the set `{f(a, b) | a ∈ s, b ∈ t}` are equal to `{f(a, b) | (a, b) ∈ s × t}`.
|
Set.iUnion₂_eq_univ_iff
theorem Set.iUnion₂_eq_univ_iff :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α},
⋃ i, ⋃ j, s i j = Set.univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j
The theorem `Set.iUnion₂_eq_univ_iff` states that for any type `α` and any type functions `ι` and `κ` determined by `ι`, and for any function `s` that maps each pair of elements `(i : ι)` and `(j : κ i)` to a set of elements of type `α`, the double indexed union over `i` and `j` of `s i j` is equal to the universal set of `α` if and only if for every element `a` of type `α`, there exist `i` and `j` such that `a` is an element of `s i j`. In mathematical terms, this theorem says that a double union of sets covers the entire universe of discourse if and only if every element of the universe is in at least one of the sets in the union.
More concisely: A double indexed union of sets equals the universe if and only if each element of the universe belongs to at least one set in the union.
|
Set.iUnion_inter
theorem Set.iUnion_inter : ∀ {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ι → Set β), (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s
This theorem states that for any type `β` and an index type `ι`, given a set `s` of type `β` and a function `t`, that maps from index type `ι` to a set of type `β`, the intersection of `s` and the union over `t i` for all `i` is equal to the union of the intersections of `s` and `t i` for all `i`. In mathematical notation, this would be:
`(⋃ i, t(i)) ∩ s = ⋃ i, (t(i) ∩ s)`
It is essentially an assertion of a distributive property of intersection over union for sets.
More concisely: The theorem asserts that for any set `s` and function `t` mapping index type `ι` to sets of type `β`, the intersection of `s` with the union of `t(i)` over all `i` is equal to the union of intersections of `s` with each `t(i)`. In mathematical notation, `(⋃ i, t(i)) ∩ s = ⋃ i, (t(i) ∩ s)`.
|
Set.biUnion_preimage_singleton
theorem Set.biUnion_preimage_singleton :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s
The theorem `Set.biUnion_preimage_singleton` states that for all types `α` and `β`, and for all functions `f` from `α` to `β` and all sets `s` of type `β`, the union over all `y` in `s` of the preimage of the singleton set `{y}` under `f` is equal to the preimage of the set `s` under `f`. In simpler terms, if we take each individual element of a set, map it back through the function `f`, and take the union of all these mapped sets, we get the same result as if we had just taken the preimage of the entire set at once.
More concisely: For all types `α` and `β`, and for all functions `f` from `α` to `β` and sets `s` of type `β`, the preimage of `s` under `f` is equal to the union of the preimages of the singleton sets `{y}` for all `y` in `s`.
|
Set.sUnion_mono_subsets
theorem Set.sUnion_mono_subsets :
∀ {α : Type u_1} {s : Set (Set α)} {f : Set α → Set α}, (∀ (t : Set α), t ⊆ f t) → s.sUnion ⊆ (f '' s).sUnion := by
sorry
The theorem `Set.sUnion_mono_subsets` states that for all types `α`, sets `s` of type `Set α`, and functions `f` from `Set α` to `Set α` that map any set `t` to a superset of `t`, the union over all sets in `s` is a subset of the union over all images of sets in `s` under the function `f`. In other words, if each set in `s` gets mapped to a larger set by `f`, then the union of the sets in `s` is contained within the union of the larger sets.
More concisely: For any type `α`, sets `s` of type `Set α`, and function `f` from `Set α` to `Set α` such that `t ⊆ f(t)` for all `t` in `s`, we have `⋃(s) ⊆ ⋃(map f s)`.
|
Set.iInter_and
theorem Set.iInter_and :
∀ {α : Type u_1} {p q : Prop} (s : p ∧ q → Set α), ⋂ (h : p ∧ q), s h = ⋂ (hp : p), ⋂ (hq : q), s ⋯
This theorem states that for any type `α` and given two propositions `p` and `q`, and a set `s` which depends on the conjunction of `p` and `q`, the intersection over `s` for every instance where both `p` and `q` hold true is the same as the nested intersection over `s` where `p` holds true and then for every instance where `q` holds true. In mathematical terms, it's saying that the intersection over a set that depends on the conjunction of two conditions is equivalent to taking the intersection twice, first for each condition separately.
More concisely: For any set `s` and propositions `p` and `q`, the intersection of `s` over instances where `p` and `q` hold true equals the intersection of `s` where `p` holds true and then the intersection of the result with where `q` holds true.
|
Set.mem_biUnion
theorem Set.mem_biUnion :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : α → Set β} {x : α} {y : β}, x ∈ s → y ∈ t x → y ∈ ⋃ x ∈ s, t x
This theorem, `Set.mem_biUnion`, states that for any types `α` and `β`, a set `s` of type `α`, a function `t` mapping from `α` to a set of type `β`, and elements `x` of type `α` and `y` of type `β`, if `x` is an element of `s` and `y` is an element of the set `t(x)`, then `y` is an element of the union over `s` of the sets `t(x)`. In mathematical notation, this would be expressed as if $x \in s$ and $y \in t(x)$, then $y \in \bigcup_{x \in s} t(x)$.
More concisely: If `x` is an element of `s` and `y` is an element of `t(x)`, then `y` is an element of the set `⋃(x ∈ s) t(x)`.
|
Set.image2_iInter_subset_left
theorem Set.image2_iInter_subset_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : ι → Set α) (t : Set β),
Set.image2 f (⋂ i, s i) t ⊆ ⋂ i, Set.image2 f (s i) t
This theorem states that for every types `α`, `β`, `γ` and a sort `ι`; for a function `f` from `α` to `β` to `γ`; for a family of sets `s` indexed by `ι` of type `α`; and for a set `t` of type `β`, the image under `f` of the intersection of all sets `s i` with set `t` is a subset of the intersection of the image under `f` of each `s i` with set `t`. In mathematical terms, it asserts that $f((\bigcap_{i} s_i) \times t) \subseteq \bigcap_{i} f(s_i \times t)$.
More concisely: For every functions $f: \alpha \to \beta \to \gamma$, sets $s\_i:\_ \to \alpha$ indexed by $ι$, and sets $t:\beta$, we have $f(\bigcap\_{i} (s\_i \times t)) \subseteq \bigcap\_{i} (f(s\_i \times t))$.
|
Function.Surjective.iUnion_comp
theorem Function.Surjective.iUnion_comp :
∀ {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ι → ι₂},
Function.Surjective f → ∀ (g : ι₂ → Set α), ⋃ x, g (f x) = ⋃ y, g y
The theorem `Function.Surjective.iUnion_comp` states that for any type `α`, sorts `ι` and `ι₂`, and a function `f` that maps from `ι` to `ι₂`, if `f` is surjective, then for any function `g` that maps from `ι₂` to a set of `α`, the union over all `x` of `g(f(x))` is equal to the union over all `y` of `g(y)`. In other words, it states that under a surjective function, the union of the images of a set-function remains unchanged.
More concisely: If `f: ι → ι₂` is a surjective function and `g: ι₂ → Å(α)` is any function, then `⋃(x ∈ ι) g(f x) = ⋃(y ∈ ι₂) g(y)`.
|
Set.preimage_sUnion
theorem Set.preimage_sUnion :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)}, f ⁻¹' s.sUnion = ⋃ t ∈ s, f ⁻¹' t
The theorem `Set.preimage_sUnion` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, and for any set `s` of sets of `β`, the preimage of the union of set `s` under the function `f` is equal to the union of the preimages of the elements in set `s` under the function `f`. In mathematical terms, it says that if `f` is a function from `α` to `β`, and `s` is a collection of subsets of `β`, then the preimage of the union of the sets in `s` is the union of the preimages of the sets in `s`. This is a formal statement of the property that preimages commute with union of sets.
More concisely: For any function `f: α -> β` and set `s` of subsets of `β`, `f ^-1 (∪ s) = ∪ (f ^-1 [s])`.
|
Set.iUnion_const
theorem Set.iUnion_const : ∀ {β : Type u_2} {ι : Sort u_4} [inst : Nonempty ι] (s : Set β), ⋃ x, s = s
The theorem `Set.iUnion_const` asserts that for any type `β`, any type `ι` (where `ι` is nonempty), and any set `s` of type `β`, the indexed union over `s` (denoted by `⋃ x, s`) is equal to `s` itself. This is equivalent to stating that the union of a constant set `s` over all elements of any nonempty indexing set `ι` results in the set `s` itself. The theorem applies regardless of the specific types `β` and `ι` involved.
More concisely: For any nonempty indexing type ι and set s of type β, the indexed union (⋃ x, s) equals set s.
|
Set.inter_iUnion
theorem Set.inter_iUnion : ∀ {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ι → Set β), s ∩ ⋃ i, t i = ⋃ i, s ∩ t i
This theorem states that for any set `s` of elements of type `β` and any indexed collection `t` of sets of elements of type `β` (indexed by elements of type `ι`), the intersection of `s` with the union of the `t` sets (over all `ι`) is equal to the union of the intersections of `s` with each `t` set (over all `ι`). In mathematical notation, this would be expressed as \(s \cap (\bigcup_i t_i) = \bigcup_i (s \cap t_i)\). This is a statement about the distributive property of intersection over union in the context of sets.
More concisely: The theorem asserts that for any set `s` and indexed family `t` of sets, the intersection of `s` with the union of the `t` sets equals the union of the intersections of `s` with each `t` set. In mathematical notation: \(s \cap (\bigcup\_{i} t\_i) = \bigcup\_{i} (s \cap t\_i)\).
|
Set.iUnion_of_singleton
theorem Set.iUnion_of_singleton : ∀ (α : Type u_11), ⋃ x, {x} = Set.univ
This theorem, named `Set.iUnion_of_singleton`, states that for any type `α`, the union over all elements `x` of the set containing only `x` is equal to the universal set of `α`. In other words, if we take every single-element set `{x}` for all `x` in `α` and unite them all together, we'll have covered the entire set of `α`. This is essentially saying that every element in the universal set `α` can be singled out into its own set, and combining these singleton sets will recover the original universal set.
More concisely: For any type `α`, the union of all singleton sets in `α` equals `α`.
|
Set.image_iUnion₂
theorem Set.image_iUnion₂ :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} (f : α → β) (s : (i : ι) → κ i → Set α),
f '' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f '' s i j
The theorem `Set.image_iUnion₂` states that for any types `α`, `β`, and `ι`, and any family of types `κ` indexed by `ι`, given a function `f` from `α` to `β`, and a double-indexed collection `s` of sets of `α`, the image under `f` of the union of all these sets (over both indices) is equal to the union of the images under `f` of each of these sets. In mathematical terms, this is saying that $f(\bigcup_{i}\bigcup_{j}s_{i,j}) = \bigcup_{i}\bigcup_{j}f(s_{i,j})$. This is a statement about the commutativity of the union operation with the image of a function operation.
More concisely: For any types `α`, `β`, and index `ι`, given a function `f` from `α` to `β` and a double-indexed family of sets `s` of `α`, the image of the union of all sets over both indices is equal to the union of the images of each set under `f`: $f(\bigcup\_{i}\bigcup\_{j}s\_{i,j}) = \bigcup\_{i}\bigcup\_{j}f(s\_{i,j})$.
|
Set.preimage_iUnion
theorem Set.preimage_iUnion :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {s : ι → Set β}, f ⁻¹' ⋃ i, s i = ⋃ i, f ⁻¹' s i := by
sorry
This theorem, referred to as `Set.preimage_iUnion`, establishes a property related to the preimage of a union of sets through a function. Specifically, for any types `α` and `β`, any indexing type `ι`, any function `f` from `α` to `β`, and any indexed collection of sets `s` from `ι` to the sets of `β`, the preimage of the union of the sets `s i` under the function `f` equals the union of the preimages of each individual set `s i` under the same function. In more mathematical language, it states that $f^{-1}(\bigcup_{i} s_i) = \bigcup_{i} f^{-1}(s_i)$, where $f^{-1}$ denotes the preimage of a set under the function `f`.
More concisely: For any function `f` from type `α` to type `β`, and any indexed collection of sets `s` from `ι` to the sets of `β`, the preimage of the union of the sets `s i` under `f` is equal to the union of the preimages of each individual set `s i` under `f`. In symbols, $f^{-1}(\bigcup\_{i} s\_i) = \bigcup\_{i} f^{-1}(s\_i)$.
|
Set.subset_iUnion₂_of_subset
theorem Set.subset_iUnion₂_of_subset :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : Set α} {t : (i : ι) → κ i → Set α} (i : ι) (j : κ i),
s ⊆ t i j → s ⊆ ⋃ i, ⋃ j, t i j
This theorem states that for any type `α` and any index types `ι` and `κ` which depend on `ι`, given a set `s` of type `α` and a function `t` that maps each element in `ι` and an element in `κ i` to a set of type `α`, if `s` is a subset of `t i j` for some `i` and `j`, then `s` is also a subset of the union over all `i` of the union over all `j` of `t i j`. In mathematical terms, if $s \subseteq t(i,j)$ for some $i$ and $j$, then $s \subseteq \bigcup_{i} \bigcup_{j} t(i,j)$.
More concisely: If for some indices i and j, a subset s of type α is contained in the set obtained by indexing and then taking the union over all i and j of a function t that maps i and a κ-index j to sets of type α, then s is contained in the overall union of all those sets obtained by indexing i and then taking the union over all j. In mathematical notation, if ∃i,j. s ⊆ t(i,j), then s ⊆ ⋃i⋃j t(i,j).
|
Set.iInter_subset
theorem Set.iInter_subset : ∀ {β : Type u_2} {ι : Sort u_4} (s : ι → Set β) (i : ι), ⋂ i, s i ⊆ s i
This theorem states that for all types `β` and `ι`, and for a function `s` mapping `ι` to a set of `β`, and for any element `i` of type `ι`, the intersection over all `i` of the sets `s i` is a subset of `s i`. This is a formalization of the standard set theory fact that any set is a subset of its superset, or in other words, any set is included in the union of all sets.
More concisely: For any function `s` mapping type `ι` to sets of type `β`, and for all `i` in `ι`, the intersection of `s i` over all `i` is a subset of `s i`.
|
Mathlib.Data.Set.Lattice._auxLemma.16
theorem Mathlib.Data.Set.Lattice._auxLemma.16 :
∀ {α : Type u_1} {s : Set (Set α)} {t : Set α}, (s.sUnion ⊆ t) = ∀ t' ∈ s, t' ⊆ t
This theorem, `Mathlib.Data.Set.Lattice._auxLemma.16`, states that for any type `α`, any set `s` of sets of `α`, and any set `t` of `α`, the union of all the sets in `s` is a subset of `t` if and only if every set `t'` that belongs to `s` is a subset of `t`. In the context of set theory, the concept of "union" (denoted by `⋃₀ s`) refers to the aggregation of all the elements in the sets in `s`, and "subset" (denoted by `⊆`) means that all elements of the first set are also elements of the second set.
More concisely: For any type `α`, set `s` of sets of `α`, and set `t` of `α`, `⋃₀ s ⊆ t` if and only if for all `s' ∈ s`, `s' ⊆ t`.
|
Set.biInter_subset_of_mem
theorem Set.biInter_subset_of_mem :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : α → Set β} {x : α}, x ∈ s → ⋂ x ∈ s, t x ⊆ t x
The `Set.biInter_subset_of_mem` theorem states that for any types `α` and `β`, a set of elements of type `α` denoted by `s`, a function `t` mapping elements of `α` to sets of `β`, and an element `x` of type `α`, if `x` is an element of set `s`, then the intersection of all sets `t x` for each `x` in `s` is a subset of `t x`. In mathematical terms, it asserts that if $x \in s$, then $\bigcap_{x \in s} t(x) \subseteq t(x)$.
More concisely: For any sets `s` of type `α` and function `t` mapping elements of `α` to sets of `β`, if `x` is an element of `s`, then `t x` is a subset of the intersection of all `t(y)` for `y` in `s`. In mathematical notation, $x \in s \implies t(x) \subseteq \bigcap\_{y \in s} t(y)$.
|
Set.subset_iInter₂
theorem Set.subset_iInter₂ :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : Set α} {t : (i : ι) → κ i → Set α},
(∀ (i : ι) (j : κ i), s ⊆ t i j) → s ⊆ ⋂ i, ⋂ j, t i j
This theorem states that for any type `α` and an indexed family of sorts `{ι : Sort u_4} {κ : ι → Sort u_7}`, given a set `s` of type `α` and a function `t` that takes an index `i` of type `ι` and a second index `j` of type `κ i` and returns a set of type `α`, if `s` is a subset of every set `t i j`, then `s` is also a subset of the intersection over all `i` and `j` of the sets `t i j`. In mathematical terms, if for all `i` and `j`, `s` is a subset of `t_i_j`, then `s` is a subset of the intersection over all `i` and `j` of the sets `t_i_j`.
More concisely: If for all indices i and j, a set s is a subset of the set t(i) (j), then s is a subset of the intersection over all i and j of the sets t(i) (j).
|
Set.subset_iUnion_of_subset
theorem Set.subset_iUnion_of_subset :
∀ {α : Type u_1} {ι : Sort u_4} {s : Set α} {t : ι → Set α} (i : ι), s ⊆ t i → s ⊆ ⋃ i, t i
This theorem states that for any type `α` and a collection of sets `t` indexed by another type `ι`, if a set `s` is a subset of `t i` for some `i` of type `ι`, then `s` is also a subset of the union of all sets in the collection `t`. Here, `s ⊆ t i` represents the subset relation and `⋃ i, t i` represents the union of all sets `t i` across all `i` in type `ι`.
More concisely: If for each index `i`, set `s` is a subset of `t i`, then `s` is a subset of the union of all sets `t i`.
|
Set.sUnion_range
theorem Set.sUnion_range : ∀ {β : Type u_2} {ι : Sort u_4} (f : ι → Set β), (Set.range f).sUnion = ⋃ x, f x
This theorem states that for any type `β` and any sort `ι`, given a function `f` that maps from `ι` to a set of `β`, the union of the sets in the range of `f` is equal to the union of the sets `f x` for every `x`. In mathematical terms, it states that the union over the range of a function `f` (i.e., ⋃₀ Set.range f) is the same as the union over all `x` of `f(x)` (i.e., ⋃ x, f x).
More concisely: For any function `f` from sort `ι` to a set of type `β`, the set union over the range of `f` equals the set union of `f(x)` for all `x` in `ι`. In Lean notation, `⋃₀ Set.range f = ⋃ x, f x`.
|
Set.iInter₂_subset_of_subset
theorem Set.iInter₂_subset_of_subset :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {t : Set α} (i : ι) (j : κ i),
s i j ⊆ t → ⋂ i, ⋂ j, s i j ⊆ t
This theorem states that for any types `α` and `ι`, any function `κ` mapping `ι` to a particular type, any function `s` that takes an element of `ι` and an element of `κ i` and returns a set of `α`, and any set `t` of `α`, if the set `s i j` (for some `i` of type `ι` and `j` of type `κ i`) is a subset of `t`, then the intersection over all `i` and `j` of the sets `s i j` is also a subset of `t`. In other words, if a particular set in a family of sets is a subset of `t`, then the intersection of all sets in the family is also a subset of `t`.
More concisely: For any types `α`, `ι`, and functions `κ: ι → Type`, `s: ι → κ i → Set α`, and `t: Set α`, if for all `i ∈ ι` and `j ∈ κ i`, `s i j ⊆ t`, then `∩ i, j in ι × κ i, s i j ⊆ t`.
|
Set.sUnion_eq_univ_iff
theorem Set.sUnion_eq_univ_iff : ∀ {α : Type u_1} {c : Set (Set α)}, c.sUnion = Set.univ ↔ ∀ (a : α), ∃ b ∈ c, a ∈ b
This theorem, `Set.sUnion_eq_univ_iff`, states that for any type `α` and any set `c` of sets of `α`, the union over all elements in `c` (denoted as `⋃₀ c`) equals the universal set of `α` (which contains all elements of `α`) if and only if for any element `a` of type `α`, there exists a set `b` in `c` such that `a` is an element of `b`. In the context of set theory, this expresses that a collection of sets covers all elements of a given type if and only if every element of the type is contained in at least one of the sets in the collection.
More concisely: For a type `α` and a set `c` of sets over `α`, `⋃₀ c` equals the universe of `α` if and only if every `α` element is in some `c` set.
|
Mathlib.Data.Set.Lattice._auxLemma.9
theorem Mathlib.Data.Set.Lattice._auxLemma.9 :
∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (y : β), (y ∈ f '' s) = ∃ x ∈ s, f x = y
This theorem, titled `Mathlib.Data.Set.Lattice._auxLemma.9`, states that for any types `α` and `β`, for any function `f` from `α` to `β`, for any set `s` of elements of type `α`, and for any element `y` of type `β`, the condition "y is in the image of set s under function f" is equivalent to saying "there exists an element x in set s such that f applied to x equals y". In other words, it characterizes membership in the image of a set under a function in terms of the existence of a pre-image under the function.
More concisely: For any functions between types and sets, an element belongs to the image of a set under the function if and only if there exists an element in the set mapping to that image under the function.
|
Set.image2_iInter_subset_right
theorem Set.image2_iInter_subset_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : Set α) (t : ι → Set β),
Set.image2 f s (⋂ i, t i) ⊆ ⋂ i, Set.image2 f s (t i)
This theorem states that for any types `α`, `β`, and `γ`, an indexing type `ι`, a binary function `f` from `α` and `β` to `γ`, a set `s` of type `α`, and a function `t` from `ι` to the set of `β`, the image under `f` of the set `s` and the intersection over `ι` of the sets `t i` is a subset of the intersection over `ι` of the images under `f` of the set `s` and the sets `t i`. In terms of mathematical notation, this can be written as $f(s, \bigcap_{i} t_i) \subseteq \bigcap_{i} f(s, t_i)$.
More concisely: For any types `α`, `β`, `γ`, indexing type `ι`, function `f` from `α × β` to `γ`, set `s` of type `α`, and function `t` from `ι` to `β`, the image of `s` under `f` intersecting the images of `t i` is a subset of the intersection of the images of `s` and `t i` for all `i`. In symbols, $f(s) \cap (\bigcap\_{i} f(s, t\_i)) \subseteq \bigcap\_{i} f(s, t\_i)$.
|
Set.subset_sUnion_of_mem
theorem Set.subset_sUnion_of_mem : ∀ {α : Type u_1} {S : Set (Set α)} {t : Set α}, t ∈ S → t ⊆ S.sUnion
The theorem `Set.subset_sUnion_of_mem` states that for any type `α`, and for any set `S` of sets of type `α`, if another set `t` of type `α` is a member of `S`, then `t` is a subset of the union over all sets in `S`, denoted by `⋃₀ S`. In other words, any element of a collection of sets is itself a subset of the union of the entire collection.
More concisely: For any type `α` and set `S` of subsets of `α`, if `t ∈ S`, then `t ⊆ ⋃₀ S`.
|
Set.iInter₂_mono
theorem Set.iInter₂_mono :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s t : (i : ι) → κ i → Set α},
(∀ (i : ι) (j : κ i), s i j ⊆ t i j) → ⋂ i, ⋂ j, s i j ⊆ ⋂ i, ⋂ j, t i j
The theorem `Set.iInter₂_mono` states that for any type `α`, and for any sorts `ι` and `κ` indexed by `ι`, given two families `(s : (i : ι) → κ i → Set α)` and `(t : (i : ι) → κ i → Set α)` of sets indexed by `ι` and `κ i`, if every set in the family `s` is a subset of the corresponding set in the family `t` (i.e., for every index `i` of type `ι` and `j` of type `κ i`, `s i j` is a subset of `t i j`), then the intersection of all sets in the family `s` is a subset of the intersection of all sets in the family `t`. In mathematical terms, if ∀(i : ι)(j : κ i), s i j ⊆ t i j, then ⋂ i, ⋂ j, s i j ⊆ ⋂ i, ⋂ j, t i j.
More concisely: If for every index `i` of type `ι` and `j` of type `κ i`, the set `s i j` is a subset of `t i j`, then the intersection of all sets `s i j` in the family indexed by `ι` and `κ i` is a subset of the intersection of all sets `t i j`.
|
Set.iUnion_eq_univ_iff
theorem Set.iUnion_eq_univ_iff :
∀ {α : Type u_1} {ι : Sort u_4} {f : ι → Set α}, ⋃ i, f i = Set.univ ↔ ∀ (x : α), ∃ i, x ∈ f i
This theorem states that for any type `α` and any indexing type `ι`, if you have a function `f` that maps from the indexing type to a set of the type `α`, then the union of all the sets `f i` (for all `i` in `ι`) equals the universal set of `α` if and only if for every element `x` of type `α`, there exists an index `i` such that `x` is an element of the set `f i`. In terms of set theory, this is saying that the union of a collection of sets covers the entire universal set if and only if every element in the universe is in at least one of the sets in the collection.
More concisely: Given a function from an indexing type to sets of a type `α`, the union of these sets equals the universal set of `α` if and only if every element of `α` is in some image set.
|
Set.mapsTo_iInter_iInter
theorem Set.mapsTo_iInter_iInter :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α} {t : ι → Set β} {f : α → β},
(∀ (i : ι), Set.MapsTo f (s i) (t i)) → Set.MapsTo f (⋂ i, s i) (⋂ i, t i)
The theorem `Set.mapsTo_iInter_iInter` states that for any types `α`, `β` and a sort `ι`, given a family of sets `{s i}` in `α` and `{t i}` in `β` indexed by `ι`, and a function `f` mapping from `α` to `β`, if for all `i` in `ι` the function `f` maps every element in `s i` into `t i` (represented by `Set.MapsTo f (s i) (t i)`), then `f` also maps every element in the intersection of all `s i` into the intersection of all `t i` (represented by `Set.MapsTo f (⋂ i, s i) (⋂ i, t i)`). In other words, if a function maps every element of each set in a family of sets to a corresponding set in another family of sets, it does the same for the intersections of those families of sets.
More concisely: If for each index `i` in `ι`, a function `f` maps every element of `s i` to `t i`, then `f` maps every element of the intersection of all `s i` to the intersection of all `t i`.
|
Mathlib.Data.Set.Lattice._auxLemma.49
theorem Mathlib.Data.Set.Lattice._auxLemma.49 : ∀ {α : Type u} (x : α), (x ∈ Set.univ) = True
This theorem states that for all types `α`, `β`, and `γ`, and for any binary function `f` from `α` and `β` to `γ`, and for any sets `s` of type `α`, `t` of type `β`, and `u` of type `γ`, the condition that the image of the binary function `f` applied to sets `s` and `t` is a subset of `u` is equivalent to the condition that for every element `x` in `s` and every element `y` in `t`, the function `f` applied to `x` and `y` results in an element that belongs to `u`. In other words, if we apply the function to each element of `s` and `t`, all resulting elements belong to `u`.
More concisely: For any types `α`, `β`, `γ`, sets `s` of type `α`, `t` of type `β`, and binary function `f` from `α` and `β` to `γ`, the image of `f` applied to `s` and `t` is a subset of `u` if and only if for all `x` in `s` and `y` in `t`, `f x y` is in `u`.
|
Set.iInter_exists
theorem Set.iInter_exists :
∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {f : Exists p → Set α},
⋂ (x : Exists p), f x = ⋂ i, ⋂ (h : p i), f ⋯
This theorem states that for any type `α` and any predicate `p` on a sort `ι`, the intersection over all sets `f x` where `x` satisfies `Exists p`, is equal to the intersection over all `i` and for each `i`, the intersection over all `h` that satisfy `p i` of `f h`. In other words, it says that intersecting over all existing `x` that satisfy a predicate `p` is the same as intersecting over all `i` and then intersecting over all `h` that satisfy `p i`.
More concisely: For any type `α` and predicate `p` on a sort `ι`, the intersection of `{f x | ∃ (x : α), p x}` is equal to the intersection of `{⋈ {i : ι} {h : i | p i} | f h}` where `⋈` denotes set intersection.
|
Set.biInter_eq_iInter
theorem Set.biInter_eq_iInter :
∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x ∈ s → Set β),
⋂ x, ⋂ (h : x ∈ s), t x h = ⋂ x, t ↑x ⋯
This theorem states that for any two types `α` and `β`, a set `s` of type `α`, and a function `t` defined for elements `x` of `α` that belong to `s` and returning a set of `β`, the intersection over `x` of the intersections (for `x` in `s`) of `t x` is equal to the intersection over `x` of `t ↑x`. Essentially, this theorem shows that for the given conditions, the order of intersections does not matter.
More concisely: For any sets `s` of type `α`, and a function `t : α → Set β` such that `x ∈ s` implies `x ∈ domain(t)`, the intersection of `{∥ ti x∥ | x ∈ s}` is equal to the intersection of `{∥ t (i x)∥ | x ∈ s}`, where `i : α → α` is the identity function.
|
Set.sInter_subset_of_mem
theorem Set.sInter_subset_of_mem : ∀ {α : Type u_1} {S : Set (Set α)} {t : Set α}, t ∈ S → S.sInter ⊆ t
The theorem `Set.sInter_subset_of_mem` states that for any type `α`, and for any set `S` of sets of `α`, and for any set `t` of `α`, if `t` is an element of `S`, then the intersection over all sets in `S` is a subset of `t`. In the language of set theory, this means if a set is part of a collection of sets, then the intersection of all those sets is included within that particular set.
More concisely: For any type `α`, if `S` is a set of sets of `α` and `t` is an element of `S`, then `∩S ⊆ t`.
|
Set.iUnion₂_mono
theorem Set.iUnion₂_mono :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s t : (i : ι) → κ i → Set α},
(∀ (i : ι) (j : κ i), s i j ⊆ t i j) → ⋃ i, ⋃ j, s i j ⊆ ⋃ i, ⋃ j, t i j
This theorem, `Set.iUnion₂_mono`, states that for any type `α` and any indexed types `ι` and `κ`, if we have two families of sets `s` and `t` indexed by `ι` and `κ`, and every set in `s` is a subset of the corresponding set in `t`, then the union over `ι` and `κ` of the sets in `s` is a subset of the union over `ι` and `κ` of the sets in `t`. In other words, if each set from one indexed collection of sets is included in the corresponding set from another collection, then the union of the first collection of sets is included in the union of the second collection.
More concisely: If for all i in ι and j in κ, s(i, j) ⊆ t(i, j), then ⋃i∈ι⋃j∈κ s(i, j) ⊆ ⋃i∈ι⋃j∈κ t(i, j).
|
Set.mem_iUnion₂_of_mem
theorem Set.mem_iUnion₂_of_mem :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {a : α} {i : ι} (j : κ i),
a ∈ s i j → a ∈ ⋃ i, ⋃ j, s i j
This theorem states that for any type `α`, an index type `ι`, a dependent type `κ` indexed by `ι`, a function `s` that given `i` of type `ι` and `j` of type `κ i` returns a set of elements of type `α`, and an element `a` of type `α`, if `a` is in the set `s i j` for some given `i` and `j`, then `a` is in the union over all `i` and `j` of the sets `s i j`. In other words, if an element belongs to a specific set in a collection of sets indexed by two parameters, it belongs to the union of these sets.
More concisely: If for all `i:` `ι` and `j:` `κ i`, `a:` `α` belongs to `s i j`, then `a` belongs to the union of all `s i j`.
|
Set.iUnion_iUnion_eq_left
theorem Set.iUnion_iUnion_eq_left :
∀ {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → x = b → Set α}, ⋃ x, ⋃ (h : x = b), s x h = s b ⋯
The theorem `Set.iUnion_iUnion_eq_left` states that for any types `α` and `β`, a given value `b` of type `β`, and a function `s` which maps each value `x` of type `β` and a proof `h` that `x` equals `b` to a set of `α`, the union over all `x` of the union over all proofs `h` that `x` equals `b` of `s x h` is equal to the set `s b` determined by any proof. In simpler terms, this theorem is about simplifying the union of unions when the inner union is over proofs of a specific equality. The resulting set is just the one associated with the specific value and any proof of its identity.
More concisely: For any types `α` and `β`, given a value `b` of type `β` and a function `s : β → Set α`, the set `s b` is equal to the union over all proofs `h : b = x` of the union of `s x h`.
|
Set.preimage_iUnion₂
theorem Set.preimage_iUnion₂ :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {f : α → β} {s : (i : ι) → κ i → Set β},
f ⁻¹' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f ⁻¹' s i j
This theorem states that, for all types `α`, `β`, `ι`, and `κ`, and for any function `f` mapping from `α` to `β`, and any function `s` mapping from `ι` to `κ`, the preimage of the union over `i` and `j` of the set `s i j` under the function `f` is equal to the union over `i` and `j` of the preimage of the set `s i j` under `f`.
In simpler terms, we are distributing the preimage operation over the union of sets, much in the same way we would distribute multiplication over addition in arithmetic.
More concisely: For all types `α`, `β`, `ι`, `κ`, functions `f : α → β`, and `s : ι → κ`, the preimage of `(⋃ i, j : ι, s i j)` under `f` equals `⋃ i, j : ι, f⁻¹(s i j)`.
|
Set.iUnion_of_empty
theorem Set.iUnion_of_empty : ∀ {α : Type u_1} {ι : Sort u_4} [inst : IsEmpty ι] (s : ι → Set α), ⋃ i, s i = ∅ := by
sorry
This theorem states that for any type `α` and an index type `ι`, if `ι` is empty (i.e., there are no elements of type `ι`), then the indexed union of sets `s i` (from `ι` to `Set α`) results in the empty set. In other words, if we have a family of sets but no indices to pick any set from that family, the union of these sets would be empty.
More concisely: If `ι` is empty, then the indexed union of sets `s i` (for `i` in `ι`) is the empty set.
|
Set.sUnion_eq_biUnion
theorem Set.sUnion_eq_biUnion : ∀ {α : Type u_1} {s : Set (Set α)}, s.sUnion = ⋃ i ∈ s, i
The theorem `Set.sUnion_eq_biUnion` states that for any type `α` and any set `s` of sets of type `α`, the union of all the sets in `s` (`⋃₀ s`) is equal to the union of all elements that belong to some set in `s` (`⋃ i ∈ s, i`). In other words, it is stating that the union over a set of sets is equivalent to the bi-union over elements in those sets.
More concisely: For any set `s` of sets over type `α`, the set theoretic union of `s` equals the bi-union over the elements in `s`. In Lean notation, `⋃₀ s = ⋃ i ∈ s, i`.
|
Set.image_preimage
theorem Set.image_preimage :
∀ {α : Type u_1} {β : Type u_2} {f : α → β}, GaloisConnection (Set.image f) (Set.preimage f)
The theorem `Set.image_preimage` states that for any types `α` and `β` and any function `f` from `α` to `β`, there exists a Galois Connection between the function `Set.image f` and the function `Set.preimage f`. A Galois Connection is a pair of functions `l` and `u` such that for all `a` in `α` and `b` in `β`, `l a` is less than or equal to `b` if and only if `a` is less than or equal to `u b`. In the context of this theorem, `Set.image f` is a function that maps a set of elements in `α` to its image in `β` under `f`, and `Set.preimage f` is a function that maps a set in `β` to its preimage in `α` under `f`.
More concisely: For any function `f` from type `α` to type `β`, there exists a Galois Connection between the image function `Set.image f` and the preimage function `Set.preimage f`.
|
Set.sUnion_eq_iUnion
theorem Set.sUnion_eq_iUnion : ∀ {α : Type u_1} {s : Set (Set α)}, s.sUnion = ⋃ i, ↑i
The theorem `Set.sUnion_eq_iUnion` states that for any type `α` and any set `s` of sets of type `α`, the set-theoretic union of all sets in `s` is equal to the union over all elements in the embedding of individual sets `i` in `s`. In mathematical terms, this means that for any collection of sets, the union of all those sets is the same as taking the union of each set one at a time.
More concisely: For any type `α` and set `s` of sets of type `α`, the set-theoretic union of all sets in `s` equals the indexed union over `s`.
|
Set.biUnion_of_singleton
theorem Set.biUnion_of_singleton : ∀ {α : Type u_1} (s : Set α), ⋃ x ∈ s, {x} = s
The theorem `Set.biUnion_of_singleton` states that for any set `s` of an arbitrary type `α`, the union over all elements `x` in the set `s` of the singleton sets containing `x` is equal to the set `s` itself. In more mathematical terms, for any set `s`, if you take every element `x` in `s`, form the singleton set `{x}`, and then take the union of all these singleton sets, you get back the original set `s`.
More concisely: For any set `s`, the union of the singleton sets `{x}` for all `x` in `s` equals `s`.
|
Set.image_iInter₂_subset
theorem Set.image_iInter₂_subset :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} (s : (i : ι) → κ i → Set α) (f : α → β),
f '' ⋂ i, ⋂ j, s i j ⊆ ⋂ i, ⋂ j, f '' s i j
This theorem states that for any two types `α` and `β`, a type indexed by a sort `ι` and a family of sets `s` indexed by `ι` and a type depending on `ι`, and a function `f` mapping elements of type `α` to type `β`, the image of the intersection of all sets in the family `s` under the function `f` is a subset of the intersection of the images of all sets in the family `s` under the function `f`. In mathematical terms, if we have a function `f: α → β` and a family of sets `s_i` for each `i` in `ι` and `j` in `κ(i)`, then `f` applied to the intersection of all `s_i` is included in the intersection of `f` applied to all `s_i`.
More concisely: For any function `f: α -> β`, family of sets `{s_i : ι -> Sort}_i`, and all `i` in `ι`, `f (intersection (ι).map (s_i)) ⊆ intersection (list.map (λ i, f (s_i i)))`.
|
Set.sUnion_mono_supsets
theorem Set.sUnion_mono_supsets :
∀ {α : Type u_1} {s : Set (Set α)} {f : Set α → Set α}, (∀ (t : Set α), f t ⊆ t) → (f '' s).sUnion ⊆ s.sUnion := by
sorry
The theorem `Set.sUnion_mono_supsets` states that for any type `α`, any set `s` of sets of `α`, and any function `f` from sets of `α` to sets of `α`, if for every set `t` of `α`, `f` maps `t` to a subset of `t`, then the union (denoted by `sUnion`) of the images of sets in `s` under `f` is a subset of the union of `s`. In other words, if `f` shrinks every set, then the union of the images of `f` is also shrunk when compared to the union of the original sets.
More concisely: If `f` is a function mapping sets of type `α` to sets of `α` such that `f(t) ⊆ t` for all `t ∈ s`, then `s.sUnion ⊆ (⋃(map f s))`.
|
Set.sInter_insert
theorem Set.sInter_insert : ∀ {α : Type u_1} (s : Set α) (T : Set (Set α)), (insert s T).sInter = s ∩ T.sInter := by
sorry
The theorem `Set.sInter_insert` states that for any type `α`, any set `s` of type `α`, and any set `T` of sets of type `α`, the intersection over the union of `s` and `T` is equivalent to the intersection of `s` and the intersection over `T`. In other words, if you insert a set `s` into a set `T` of sets and then take the intersection over the resulting set, it's the same as intersecting `s` with the intersection over the original set `T`. This theorem generalizes one of the basic laws of intersection for sets.
More concisely: For any type `α`, set `s` of type `α`, and set `T` of sets of type `α`, `s ∩ (⋃ ts) = ⋃ (s ∩ ts : _[_] :: _[_] := T)`.
|
Set.biUnion_univ
theorem Set.biUnion_univ : ∀ {α : Type u_1} {β : Type u_2} (s : α → Set β), ⋃ x ∈ Set.univ, s x = ⋃ x, s x
This theorem, `Set.biUnion_univ`, states that for all types `α` and `β`, and for any function `s` that maps elements of `α` to sets of `β`, the union over all elements of `s` where the elements are in the universal set of `α` is equal to the union over all elements of `s`. In other words, it's saying that when we form a union of sets using elements from the universal set, it's the same as just forming a union over all sets produced by function `s`. This is a reflection of the fact that the universal set contains all elements of the type.
More concisely: For any function `s` mapping elements of type `α` to sets of type `β`, the union of `s ↥ X` (image of `X` under `s`) equals the set `⋃x ∈ X. s x`, where `X` is the universal set of type `α`.
|
Set.compl_sUnion
theorem Set.compl_sUnion : ∀ {α : Type u_1} (S : Set (Set α)), S.sUnionᶜ = (compl '' S).sInter
This theorem states that for any type `α` and a set `S` of subsets of `α`, the complement of the union of all subsets in `S` is equal to the intersection of the complements of all subsets in `S`. In other words, it expresses De Morgan's law for sets: the complement of the union is the intersection of the complements. In terms of mathematical notation, given a set `S` of subsets of a universal set `U`, it asserts that the equality `(⋃₀ S)ᶜ = ⋂₀ (compl '' S)` holds, where `⋃₀ S` denotes the union of all subsets in `S`, `⋂₀` denotes the intersection over all subsets, `ᶜ` denotes set complement, and `compl '' S` is the image of `S` under the complement function.
More concisely: The complement of the union of a set of subsets is equal to the intersection of the complements of those subsets. (De Morgan's law for sets)
|
Set.image2_eq_iUnion
theorem Set.image2_eq_iUnion :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β),
Set.image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}
The theorem `Set.image2_eq_iUnion` states that for all types `α`, `β`, and `γ`, and for any binary function `f` from `α` and `β` to `γ`, and for any sets `s` of type `α` and `t` of type `β`, the image of the binary function `f` applied to the sets `s` and `t` is equal to the union over all elements `i` in `s` and `j` in `t` of the singleton set `{f i j}`. In mathematical terms, it shows that the image of a function on a Cartesian product of two sets is the same as the union of the images of the function on individual pairs of elements, one from each set.
More concisely: For any types `α`, `β`, and `γ`, and any binary function `f` from `α × β` to `γ`, the image of `f` applied to sets `s ∈ Set α` and `t ∈ Set β` is equal to the union of the singleton sets `{f x y} | x ∈ s, y ∈ t`.
|
Set.compl_iUnion₂
theorem Set.compl_iUnion₂ :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} (s : (i : ι) → κ i → Set α),
(⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ
This theorem states that for any type `α` and two index types `ι` and `κ`, given a function `s` that generates a set of elements of type `α` for each pair of indices `(i, j)` where `i` is of type `ι` and `j` is of type `κ(i)`, the complement (i.e., set of elements not contained in the set) of the union over all `i` and `j` of the sets `s i j` is equal to the intersection over all `i` and `j` of the complements of the sets `s i j`. This theorem is a generalization of De Morgan's laws to infinite unions and intersections. In mathematical notation, it can be written as $(\bigcup_{i, j} s(i, j))^c = \bigcap_{i, j} s(i, j)^c$.
More concisely: The complement of the union of all sets indexed by pairs of types `ι` and `κ(ι)` from a function `s` is equal to the intersection of the complements of those sets. In mathematical notation: $(⋃_{i:\_} ⋃_{j:\kappa(i)} s(i, j))^c = ⋂_{i:\_} ∣_{j:\kappa(i)} s(i, j)^c$.
|
Set.iUnion_mono'
theorem Set.iUnion_mono' :
∀ {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {s : ι → Set α} {t : ι₂ → Set α},
(∀ (i : ι), ∃ j, s i ⊆ t j) → ⋃ i, s i ⊆ ⋃ i, t i
The theorem `Set.iUnion_mono'` states that for all types `α`, `ι`, and `ι₂`, and given two functions `s` and `t` that map from `ι` and `ι₂` to a set of `α` respectively, if for every element `i` of type `ι`, there exists an element `j` such that the set `s i` is a subset of the set `t j`, then the union over all `i` of the sets `s i` is a subset of the union over all `i` of the sets `t i`. In mathematical terms, this theorem asserts that if every set in a collection `{s_i}` is contained in some set in another collection `{t_j}`, then the union of the collection `{s_i}` is contained in the union of the collection `{t_j}`.
More concisely: If for each element `i` in `ι`, there exists `j` in `ι₂` such that `s i ⊆ t j`, then `⋃i.s i ⊆ ⋃j.t j`.
|
Set.compl_sInter
theorem Set.compl_sInter : ∀ {α : Type u_1} (S : Set (Set α)), S.sInterᶜ = (compl '' S).sUnion
The theorem `Set.compl_sInter` states that for any type `α`, and for any set `S` of sets of `α`, the complement of the intersection over all sets in `S` is equal to the union of the complements of all sets in `S`. In other words, for all `α` and `S`, the complement of the set of all elements that are in every set in `S` is the set of all elements that are not in at least one set in `S`. This is a formalisation of De Morgan's laws for sets.
More concisely: For any type `α` and set `S` of subsets of `α`, `Set.compl_sInter` asserts that `(∀s ∈ S, s).compl = ∧ s ∈ S, s.compl`.
This statement represents the De Morgan's laws for sets, stating that the complement of the intersection of all sets in `S` is equal to the union of the complements of those sets.
|
Set.union_eq_iUnion
theorem Set.union_eq_iUnion : ∀ {α : Type u_1} {s₁ s₂ : Set α}, s₁ ∪ s₂ = ⋃ b, bif b then s₁ else s₂
The theorem `Set.union_eq_iUnion` states that for any type `α` and for any two sets `s₁` and `s₂` of this type, the union of `s₁` and `s₂` is equal to the union over all boolean values `b`, where for each boolean, if it is true, the associated set is `s₁`, otherwise it is `s₂`. In other words, this theorem shows that the union of two sets can be expressed as a union over a boolean-indexed collection of these same two sets.
More concisely: For any type `α` and sets `s₁` and `s₂`, the union of `s₁` and `s₂` equals the indexed union over boolean values `b` where `b` maps to `s₁` if `b` is `true` and to `s₂` if `b` is `false`.
|
Set.subset_iInter
theorem Set.subset_iInter :
∀ {β : Type u_2} {ι : Sort u_4} {t : Set β} {s : ι → Set β}, (∀ (i : ι), t ⊆ s i) → t ⊆ ⋂ i, s i
The theorem `Set.subset_iInter` states that for all types `β` and `ι`, and for a set `t` of type `β` and a function `s` of type `ι` to `Set β`, if `t` is a subset of `s i` for all `i` in `ι`, then `t` must be a subset of the intersection of all `s i`. In simpler terms, if a set `t` is contained in each of a collection of sets, then it is also contained in their intersection.
More concisely: If a set is subset of every set in a family, then it is a subset of their intersection.
|
Set.subset_iUnion
theorem Set.subset_iUnion : ∀ {β : Type u_2} {ι : Sort u_4} (s : ι → Set β) (i : ι), s i ⊆ ⋃ i, s i
The theorem `Set.subset_iUnion` states that, for any type `β` and an indexing type `ι`, any set `s` indexed by `ι` is a subset of the union over all `i` in `ι` of the sets `s i`. In other words, for every index `i`, the set `s i` is contained within the union of all the sets `s i` for each `i` in the indexing type `ι`. This is a general concept in set theory, where any member of a collection of sets is necessarily a subset of the union of the entire collection of sets.
More concisely: For any indexed family of sets `{s i | i ∈ ι}`, the set `s` is a subset of their union `⋃i∈ι si`.
|
Mathlib.Data.Set.Lattice._auxLemma.1
theorem Mathlib.Data.Set.Lattice._auxLemma.1 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋃ i, s i) = ∃ i, x ∈ s i
This theorem states that for any type `α`, any sort `ι`, any element `x` of type `α`, and any indexed family of sets `s` of type `α` indexed by `ι`, the membership of `x` in the union of all sets in the family `s` is equivalent to the existence of an index `i` such that `x` is a member of the set `s i`. In other words, an element belongs to the union of a collection of sets if and only if it belongs to at least one of the sets in the collection.
More concisely: For any type `α`, sort `ι`, element `x` of type `α`, and indexed family `s` of sets over `α` indexed by `ι`, `x ∈ ⋃ i, s i <--> ∃ i, x ∈ s i`.
|
Set.iUnion_or
theorem Set.iUnion_or :
∀ {α : Type u_1} {p q : Prop} (s : p ∨ q → Set α), ⋃ (h : p ∨ q), s h = (⋃ (i : p), s ⋯) ∪ ⋃ (j : q), s ⋯ := by
sorry
This theorem, named `Set.iUnion_or`, states that for any type `α` and for any two propositions `p` and `q`, given a set `s` that is defined for the disjunction (or operation) `p ∨ q`, the indexed union over `s` for the condition `p ∨ q` is equal to the union of the indexed union over `s` for the condition `p` and the indexed union over `s` for the condition `q`. In other words, it is saying that we can distribute the "indexed union" operation over the "or" operation.
More concisely: For any type `α` and propositions `p` and `q` over a set `s`, the indexed union of `s` over `p lor q` equals the indexed union of `s` over `p` union the indexed union of `s` over `q`. (Here, `lor` is Lean's notation for the disjunction (or) operation.)
|
Set.iInter_iInter_eq_right
theorem Set.iInter_iInter_eq_right :
∀ {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → b = x → Set α}, ⋂ x, ⋂ (h : b = x), s x h = s b ⋯
This theorem states that for any types `α` and `β`, a specific element `b` of type `β`, and a function `s` that maps an element of type `β` and a proof that it equals `b` to a set of type `α`, the intersection over all `x` of the intersection over all proofs `h : b = x` of `s x h` is equal to `s b rfl`. In simpler terms, it's saying that intersecting over all possible sets generated by `s` for different inputs equivalent to `b`, results in the set generated by `s` for `b` itself.
More concisely: For any types `α` and `β`, function `s : β -> Set α`, and `b : β`, the intersections over all `x : β` and all proofs `h : b = x` are equal: `∩x (∩h (s x h)) = s b rfl`.
|
Set.sUnion_image
theorem Set.sUnion_image :
∀ {α : Type u_1} {β : Type u_2} (f : α → Set β) (s : Set α), (f '' s).sUnion = ⋃ x ∈ s, f x
The theorem `Set.sUnion_image` states that for all types `α` and `β`, for every function `f` from `α` to a set of `β`, and for every set `s` of `α`, the union over the image of `s` under `f` is equal to the union over all `x` in `s` of `f(x)`. In other words, it expresses that applying a function to each element of a set and then taking the union of the results is the same as first taking the union over the set and then applying the function. This theorem is a fundamental property of sets and functions.
More concisely: For any type `α`, set `s` of `α`, function `f` from `α` to a set, the union of `f''s` (image of `s` under `f`) is equal to the set `{x ∈ ⋃(s : Set α) : ∃(x' ∈ s). x = f(x')}`.
|
Mathlib.Data.Set.Lattice._auxLemma.33
theorem Mathlib.Data.Set.Lattice._auxLemma.33 : ∀ {α : Type u} {s t : Set α}, (s = t) = ∀ (x : α), x ∈ s ↔ x ∈ t := by
sorry
The theorem `Mathlib.Data.Set.Lattice._auxLemma.33` states that for any type `α` and any two sets `s` and `t` of type `α`, the assertion that `s` is equal to `t` is equivalent to the statement that for all elements `x` of type `α`, `x` is an element of set `s` if and only if `x` is an element of set `t`. In other words, two sets are considered equal if and only if they contain exactly the same elements.
More concisely: Two sets are equal if and only if they have the same elements.
|
Set.iUnion_iUnion_eq'
theorem Set.iUnion_iUnion_eq' :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → α} {g : α → Set β},
⋃ x, ⋃ y, ⋃ (_ : f y = x), g x = ⋃ y, g (f y)
This theorem, `Set.iUnion_iUnion_eq'`, states that for any types `α` and `β`, and an index type `ι`, given a function `f : ι → α` and another function `g : α → Set β`, the union over `x` of the union over `y` of the union over the condition that `f y = x` of `g x` is equal to the union over `y` of `g (f y)`. In other words, this theorem is about a change of order of set unions, where the function `f` maps the index `y` to an element `x`, and `g` maps this `x` to a set of `β` type elements: it guarantees that we can directly map `y` to the set of `β` elements via composition of `f` and `g`, and take the union over `y` instead of over `x`. This kind of reordering is often useful in mathematical proofs involving indexed families of sets.
More concisely: For any types α and β, and an index type ι, given functions f : ι → α and g : α → Set β, the union over y of g (f y) is equal to the union over x of the union over y with f y = x of g x.
|
Set.iInter_comm
theorem Set.iInter_comm :
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (s : ι → ι' → Set α), ⋂ i, ⋂ i', s i i' = ⋂ i', ⋂ i, s i i' := by
sorry
The theorem `Set.iInter_comm` states that for any type `α`, and any two sorts `ι` and `ι'`, the order of two nested intersection operations over sets `s` indexed by `ι` and `ι'`, does not change the resulting set. More concretely, for any function `s` that takes in two indices `i` from `ι` and `i'` from `ι'` and returns a set of type `α`, the intersection over all `i` of the intersections over all `i'` of `s i i'` is equal to the intersection over all `i'` of the intersections over all `i` of `s i i'`. This theorem essentially states the commutativity of multiple intersections over sets.
More concisely: For any function giving sets indexed by types `ι` and `ι'`, the order of intersecting over `ι'` then `ι` is equal to intersecting over `ι` then `ι'`.
|
Set.biUnion_image
theorem Set.biUnion_image :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set γ} {f : γ → α} {g : α → Set β},
⋃ x ∈ f '' s, g x = ⋃ y ∈ s, g (f y)
This theorem, `Set.biUnion_image`, states that for all types `α`, `β`, and `γ`, and for a given set `s` of type `γ`, a function `f` from `γ` to `α`, and a function `g` from `α` to a set of type `β`, the union over `x` in the image of `s` under `f` of `g(x)` is equal to the union over `y` in `s` of `g(f(y))`. In other words, it shows that the ordering of function application and set union operation can be swapped without changing the result. This theorem is a manifestation of the interchange between the operations of union and function application (image) in the context of set theory.
More concisely: For any sets `α`, `β`, `γ`, a set `s` of type `γ`, and functions `f: γ → α` and `g: α → β`, the image of `s` under `f` followed by `g` is equal to the union of `g`'s images over the elements of `s`, i.e., `(∪ y ∈ s (g ∘ f) y) = ∪ x ∈ ∫ x ∈ s g (f x)`.
|
Set.iUnion_mono
theorem Set.iUnion_mono :
∀ {α : Type u_1} {ι : Sort u_4} {s t : ι → Set α}, (∀ (i : ι), s i ⊆ t i) → ⋃ i, s i ⊆ ⋃ i, t i
The theorem `Set.iUnion_mono` states that for any type `α` and any index type `ι`, if `s` and `t` are two indexed families of sets of `α` such that every set `s i` is a subset of `t i` for each index `i` in `ι`, then the union over all `s i` (denoted as `⋃ i, s i`) is a subset of the union over all `t i` (denoted as `⋃ i, t i`). This theorem is asserting a kind of monotonicity property of indexed union operation over sets: if each individual set in one family is contained in the corresponding set in another family, then the whole union of the first family is contained in the union of the second one.
More concisely: If for each index `i`, set `s i` is a subset of `t i`, then the indexed union of `s` is a subset of the indexed union of `t`. In symbols, `⋃ i, s i ⊆ ⋃ i, t i`.
|
Set.biUnion_empty
theorem Set.biUnion_empty : ∀ {α : Type u_1} {β : Type u_2} (s : α → Set β), ⋃ x ∈ ∅, s x = ∅
The theorem `Set.biUnion_empty` states that for any types `α` and `β`, and any function `s` from `α` to a set of `β`s, the union, over all elements `x` in the empty set, of the sets `s x`, is the empty set. In other words, if you try to form a union of sets based off elements from an empty set, the result will be an empty set. This is because there are no elements in the empty set to begin with, so there are no sets to take the union of.
More concisely: The union of the empty set of elements with respect to any function mapping each element to a set, results in the empty set.
|
Set.iInter_const
theorem Set.iInter_const : ∀ {β : Type u_2} {ι : Sort u_4} [inst : Nonempty ι] (s : Set β), ⋂ x, s = s
This theorem, `Set.iInter_const`, states that for any set `s` of type `β`, and for any index `ι`, the intersection over all `x` in `ι` of `s` is equal to `s` itself. Here, `ι` represents an index set and `Nonempty ι` indicates that the index set is not empty. In other words, the intersection of the set `s` with itself for all indices in a non-empty index set is the set `s` itself. This can be expressed in mathematical terms as: for any set $s$, $\bigcap_{x \in I} s = s$, where $I$ is a non-empty index set.
More concisely: For any set `s` and non-empty index set `ι`, the intersection of `s` with itself over all indices in `ι` equals `s`. In mathematical notation: $\bigcap\_{x \in ι} s = s$.
|
Set.subset_iInter₂_iff
theorem Set.subset_iInter₂_iff :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : Set α} {t : (i : ι) → κ i → Set α},
s ⊆ ⋂ i, ⋂ j, t i j ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j
The theorem `Set.subset_iInter₂_iff` states that for any type `α`, an indexing type `ι`, a set `s` of type `α`, and a function `t` that for every index `i` of type `ι` returns a set of type `α` indexed by `κ i`, the set `s` is a subset of the intersection of all these sets (often denoted by `⋂ i, ⋂ j, t i j`) if and only if for every `i` of type `ι` and `j` of type `κ i`, `s` is a subset of `t i j`. In mathematical terms, this theorem is stating that a set `s` is a subset of the intersection of all sets in a family of sets (indexed by two indices) if and only if `s` is a subset of each individual set in the family.
More concisely: A set is a subset of the intersection of indexed sets if and only if it is a subset of each indexed set.
|
Set.iUnion_comm
theorem Set.iUnion_comm :
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (s : ι → ι' → Set α), ⋃ i, ⋃ i', s i i' = ⋃ i', ⋃ i, s i i' := by
sorry
This theorem, `Set.iUnion_comm`, states that for any type `α`, and any two types of indices `ι` and `ι'`, if `s` is a function that maps pairs of indices `(i, i')` from `ι` and `ι'` respectively to a set of type `α`, then the union over all `i` of the union over all `i'` of `s i i'` is equal to the union over all `i'` of the union over all `i` of `s i i'`. In other words, the order of taking unions does not affect the final result, which mirrors the commutative property in set theory.
More concisely: For any function `s : ∀ i i', α × α → Set α`, the sets `(⋃ i, ⋃ i' in I × I', s i i')` and `(⋃ i' in I', ⋃ i in I, s i i')` are equal.
|
Mathlib.Data.Set.Lattice._auxLemma.13
theorem Mathlib.Data.Set.Lattice._auxLemma.13 : ∀ {α : Type u} {s : Set α}, s.Nonempty = (s ≠ ∅)
The theorem `Mathlib.Data.Set.Lattice._auxLemma.13` states that for all types `α` and for all sets `s` of type `α`, the property that the set `s` is nonempty is equivalent to the assertion that the set `s` is not the empty set. Here, a set is said to be nonempty if there exists at least one element in it, and is said to be empty if it contains no elements. This theorem provides an equivalence between these two ways of expressing the notion of a nonempty set.
More concisely: The theorem asserts that a set is nonempty if and only if it is not empty.
|
Mathlib.Data.Set.Lattice._auxLemma.28
theorem Mathlib.Data.Set.Lattice._auxLemma.28 : ∀ {α : Type u} {s : Set α}, (s = ∅) = ∀ (x : α), x ∉ s
This theorem, named `Mathlib.Data.Set.Lattice._auxLemma.28`, states that for any type `α` and any set `s` of type `α`, the condition `s = ∅` (s is an empty set) is equivalent to the statement that for every element `x` of type `α`, `x` is not an element of `s` (`x ∉ s`). In simpler terms, it says that a set is empty if and only if no element of its base type is in the set.
More concisely: A set is empty if and only if no element belongs to it.
|
Set.image_iUnion
theorem Set.image_iUnion :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {s : ι → Set α}, f '' ⋃ i, s i = ⋃ i, f '' s i := by
sorry
This theorem states that for any types `α` and `β`, for an arbitrary type `ι`, for any function `f` from `α` to `β`, and for any function `s` that assigns a set of `α` to each value of `ι`, the image under `f` of the union (over `ι`) of the sets `s i` is equal to the union (over `ι`) of the images of the sets `s i` under `f`. In other words, this is a formal statement of the property of the image of a union under a function, namely that the image of the union is the union of the images, written in terms of sets. This can be written in mathematical notation as: \(f\left(\bigcup\limits_{i} s_i\right) = \bigcup\limits_{i} f\left(s_i\right)\).
More concisely: For any functions `f: α -> β` and `s: ι -> set α`, the image of the union of `s i` under `f` is equal to the union of the images of `s i` under `f`. In mathematical notation, `f(⋃i in ι s i) = ⋃i in ι (fs i)`.
|
Set.iUnion_congr_Prop
theorem Set.iUnion_congr_Prop :
∀ {α : Type u_1} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q),
(∀ (x : q), f₁ ⋯ = f₂ x) → Set.iUnion f₁ = Set.iUnion f₂
This theorem states that for any type `α`, given two predicates `p` and `q`, and two functions `f₁` and `f₂` that map from these predicates to sets of type `α`, if `p` is logically equivalent to `q` (i.e., `p ↔ q`) and for all `x` in `q`, `f₁` applied to some arguments equals `f₂` applied to `x`, then the indexed union of the sets produced by `f₁` is equal to the indexed union of the sets produced by `f₂`. In other words, if two predicates are equivalent and their corresponding set-producing functions yield the same sets, then the union of these sets is the same regardless of which predicate and function are used.
More concisely: If two predicates are logically equivalent and their corresponding functions map equivalent sets to equal sets, then the indexed unions of these sets are equal.
|
Set.image_iInter_subset
theorem Set.image_iInter_subset :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ι → Set α) (f : α → β), f '' ⋂ i, s i ⊆ ⋂ i, f '' s i := by
sorry
The theorem `Set.image_iInter_subset` states that for any types `α` and `β`, and for any indexing type `ι`, given a function `f` from `α` to `β` and a mapping `s` from `ι` to a set of `α`, the image under `f` of the intersection over all `ι` of `s i` is a subset of the intersection over all `ι` of the image of `s i` under `f`. In mathematical terms, for every function `f: α → β` and for every family of sets `(s_i)_{i in ι}`, we have `f([⋂ i, s_i]) ⊆ ⋂ i, f(s_i)`.
More concisely: For any function `f: α → β` and family of sets `(s\_i): ι → Set α`, we have `f(⋂ i, s\_i) ⊆ ⋂ i, f(s\_i)`.
|
Set.pi_def
theorem Set.pi_def :
∀ {α : Type u_1} {π : α → Type u_11} (i : Set α) (s : (a : α) → Set (π a)),
i.pi s = ⋂ a ∈ i, Function.eval a ⁻¹' s a
This theorem, `Set.pi_def`, establishes the identity of the pi set of a function over a certain domain to an intersection of pre-images. More precisely, for any type `α` and a type-valued function `π` on `α`, and for any set `i` of `α` and a set-valued function `s` on `α`, the pi set of `i` and `s`, denoted `Set.pi i s`, is equal to the intersection of sets `Function.eval a ⁻¹' s a` for all `a` in `i`. In other words, `Set.pi i s` is the set of all functions `f` such that for each index `a` in `i`, `f(a)` is in the set `s a`. This theorem states that this set is equivalent to the intersection of all pre-images of `s a` under the function `Function.eval a`, as `a` ranges over `i`.
More concisely: The pi set of a function's domain and a set-valued function is equal to the intersection of the pre-images of the set under the function evaluation at each index in the domain.
|
Set.iInter_iInter_eq_or_left
theorem Set.iInter_iInter_eq_or_left :
∀ {α : Type u_1} {β : Type u_2} {b : β} {p : β → Prop} {s : (x : β) → x = b ∨ p x → Set α},
⋂ x, ⋂ (h : x = b ∨ p x), s x h = s b ⋯ ∩ ⋂ x, ⋂ (h : p x), s x ⋯
The theorem `Set.iInter_iInter_eq_or_left` states that for any types `α` and `β`, any element `b` of type `β`, any predicate `p` on `β`, and any function `s` mapping each `β` and a proof that it equals `b` or satisfies `p` to a set of `α`, the intersection over all `β` of the intersection over all proofs that the `β` equals `b` or satisfies `p` of `s` applied to the `β` and the proof, is equal to the intersection of `s` applied to `b` and the trivial proof that `b` equals `b` or `b` satisfies `p`, and the intersection over all `β` of the intersection over all proofs that the `β` satisfies `p` of `s` applied to the `β` and the proof. In simpler terms, this theorem essentially states a specific property of intersecting sets given a certain condition or predicate.
More concisely: For any types `α` and `β`, any element `b` of type `β`, any predicate `p` on `β`, and any function `s`, the intersections of `s` over all proofs that each `β` equals `b` or satisfies `p`, are equal to the intersection of `s` applied to `b` with the trivial proof, and the intersection of `s` over all proofs that each `β` satisfies `p`.
|
Set.prod_iUnion
theorem Set.prod_iUnion :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : Set α} {t : ι → Set β}, s ×ˢ ⋃ i, t i = ⋃ i, s ×ˢ t i := by
sorry
This theorem, `Set.prod_iUnion`, states that for any type `α`, another type `β`, an index type `ι`, a set `s` of type `α` and a function `t` that maps from index `ι` to sets of type `β`, the Cartesian product of `s` and the union over `t i` for all `i` in `ι` is equal to the union over the Cartesian product of `s` and each `t i`. In simpler terms, we are distributing the Cartesian product over the union, similar to the distribution law in algebra.
More concisely: For any set `s` of type `α` and a family `(t\_i : β → Set) i in ι`, the Cartesian product `s × ⋃i in ι (t\_i)` is equal to `⋃i in ι (s × t\_i)`.
|
Set.iUnion_diff
theorem Set.iUnion_diff : ∀ {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ι → Set β), (⋃ i, t i) \ s = ⋃ i, t i \ s
This theorem states that for any type `β`, any indexing type `ι`, any set `s` of type `β`, and any indexed family of sets `t` of type `β` indexed by `ι`, the difference between the union of all `t i` and `s` is equal to the union of the differences between each `t i` and `s`. In mathematical notation, it says that $(\bigcup_i t_i) \setminus s = \bigcup_i (t_i \setminus s)$. This is a property about the interaction between the operations of union and set difference.
More concisely: For any type `β`, indexing type `ι`, set `s` of type `β`, and indexed family `t` of sets of type `β` indexed by `ι`, the difference between the union of `t` and `s` is equal to the union of the differences between each `t i` and `s`. In mathematical notation, $(\bigcup_i t_i) \setminus s = \bigcup_i (t_i \setminus s)$.
|
Set.image2_iInter₂_subset_left
theorem Set.image2_iInter₂_subset_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} (f : α → β → γ)
(s : (i : ι) → κ i → Set α) (t : Set β), Set.image2 f (⋂ i, ⋂ j, s i j) t ⊆ ⋂ i, ⋂ j, Set.image2 f (s i j) t
The theorem `Set.image2_iInter₂_subset_left` states that for any types `α`, `β`, `γ`, an index type `ι`, a dependent type `κ` indexed by `ι`, a binary function `f` from `α` and `β` to `γ`, a two-level nested indexed family of sets of `α` elements `s`, and a set `t` of `β`, the image under `f` of the intersection over all `i` and `j` of `s i j` and `t` is a subset of the intersection over all `i` and `j` of the image under `f` of `s i j` and `t`. This theorem basically asserts that the image of the intersection is a subset of the intersection of the images in a specific context involving double-indexed families of sets and a binary function.
More concisely: For any types α, β, γ, index type ι, dependent type κ over ι, binary function f from α × β to γ, sets s i j of α, and set t of β, the image under f of the intersection over all i and j of s i j and t is a subset of the intersection over all i and j of the images under f of s i j and t.
|
Mathlib.Data.Set.Lattice._auxLemma.10
theorem Mathlib.Data.Set.Lattice._auxLemma.10 :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, (a ∈ f ⁻¹' s) = (f a ∈ s)
This theorem states that for any types `α` and `β`, given a function `f : α → β`, a set `s` of type `β`, and an element `a` of type `α`, `a` is in the preimage of `s` under `f` if and only if the image of `a` under `f` is in `s`. In other words, an element maps into a set if and only if it is in the preimage of that set.
More concisely: For any function `f : α → β` and set `s ∈ β`, an element `a ∈ α` is in the preimage `f⁻¹[s]` of `s` under `f` if and only if `f(a) ∈ s`.
|
Set.biInter_subset_biInter_left
theorem Set.biInter_subset_biInter_left :
∀ {α : Type u_1} {β : Type u_2} {s s' : Set α} {t : α → Set β}, s' ⊆ s → ⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t x
This theorem states that for any two types `α` and `β`, any two sets `s` and `s'` of type `α`, and a function `t` mapping from `α` to a set of type `β`, if `s'` is a subset of `s`, then the intersection over all elements in `s` of `t(x)` is a subset of the intersection over all elements in `s'` of `t(x)`. In mathematical terms, if $s' \subseteq s$, then $\bigcap_{x \in s} t(x) \subseteq \bigcap_{x \in s'} t(x)$. It essentially highlights the fact that narrowing the range of the intersection (from `s` to `s'`) does not extend the result.
More concisely: If `s'` is a subset of `s` for types `α` and sets `s` and `s'` of `α`, and `t` is a function from `α` to a set of type `β`, then $\bigcap_{x \in s'} t(x) \subseteq \bigcap_{x \in s} t(x)$.
|
Set.iInter_iInter_eq'
theorem Set.iInter_iInter_eq' :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → α} {g : α → Set β},
⋂ x, ⋂ y, ⋂ (_ : f y = x), g x = ⋂ y, g (f y)
This theorem states that for any types `α` and `β`, and any index type `ι`, given a function `f` from `ι` to `α` and a function `g` from `α` to `Set β` (which maps elements of `α` to sets of `β`), the intersection over `x` of the intersections over `y` and `h` (where `h` is the hypothesis that `f y = x`) of `g x` is equal to the intersection over `y` of `g (f y)`. In mathematical terms, this theorem provides a new expression for the intersection of sets: $\bigcap_x \bigcap_y \bigcap_{f(y)=x} g(x) = \bigcap_y g(f(y))$. This expression can be particularly helpful when working with complex nested intersections.
More concisely: For any functions $f: ι → α$ and $g: α → Set(β)$, the intersections commute: $\bigcap\_x \bigcap\_y \{y : ι | f(y) = x\} \subseteq g(x) ∣ f(y) = x \} = \bigcap\_y g(f(y))$.
|
Set.kernImage_eq_compl
theorem Set.kernImage_eq_compl :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Set.kernImage f s = (f '' sᶜ)ᶜ
This theorem states that for any types `α` and `β`, any function `f` from `α` to `β`, and any set `s` of type `α`, the kernel image of `f` and `s` is equal to the double complement of the image of the complement of `s` under `f`. In other words, the set of all `β`-values `y` such that all preimages of `y` under `f` are within `s`, is the same as the set of all `β`-values that are not mapped to by `f` from outside `s`.
More concisely: The kernel of a function `f` from type `α` to type `β` applied to a set `s` of type `α` is equal to the complement of the image of the complement of `s` under `f`.
|
Set.iInter_true
theorem Set.iInter_true : ∀ {α : Type u_1} {s : True → Set α}, Set.iInter s = s trivial
This theorem states that for any type `α` and a function `s` from the truth value `True` to a set of elements of type `α`, the indexed intersection of this function (which represents a collection of sets) is equal to the set produced by applying the function `s` to the proof of `True`. In other words, for a set defined by a function from `True` (which is always true), the intersection of all such sets (indexed by the truth value) is simply the set associated with `True`.
More concisely: For any function `s` from `True` to a type `α`, the indexed intersection of sets `{x | s (true) x}` is equal to the image of `s` applied to the proof of `True`.
|
Set.iUnion_singleton_eq_range
theorem Set.iUnion_singleton_eq_range : ∀ {α : Type u_11} {β : Type u_12} (f : α → β), ⋃ x, {f x} = Set.range f := by
sorry
The theorem `Set.iUnion_singleton_eq_range` states that for any given function `f` mapping from a type `α` to a type `β`, the union of singleton sets `{f x}` for all `x` of type `α` is equal to the range of the function `f`. In mathematical terms, it says that for any function `f : α → β`, the set of all values `f(x)` for `x` in `α` (denoted as `⋃ x, {f x}` in Lean) is exactly the set of all possible outputs of the function `f`, also known as the range of `f`.
More concisely: For any function f : α → β, the set {fx | x ∈ α} equals the range of f.
|
Set.iUnion_iUnion_eq_right
theorem Set.iUnion_iUnion_eq_right :
∀ {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → b = x → Set α}, ⋃ x, ⋃ (h : b = x), s x h = s b ⋯
This theorem states that for any types `α` and `β`, any element `b` of type `β`, and any function `s` that assigns to each element `x` of type `β` and proof `h` that `b = x`, a set of elements of type `α`, the union over all `x` of the union over all proofs `h` that `b = x` of the set `s x h` is equal to the set `s b _`. In layman terms, it's saying that if we have a collection of sets indexed by elements of type `β` and proofs that these elements are equal to a fixed element `b`, then taking the union of these sets is the same as just considering the set corresponding to the element `b` itself.
More concisely: For any types `α` and `β`, any element `b` of type `β`, and any function `s` from `β × Prop` to `Set α`, the set `{x : β | ∃ (h : b = x), x ∈ s x h}` is equal to `s b _`.
|
Set.iUnion_true
theorem Set.iUnion_true : ∀ {α : Type u_1} {s : True → Set α}, Set.iUnion s = s trivial
This theorem states that for any type `α` and for any function `s` that maps the `True` proposition to a set of `α`, the indexed union over `s` is equal to `s` applied to the proof of `True` (which is `trivial`). This essentially means that if we take the union of sets indexed by the `True` proposition, we just get the set associated with `True` itself.
More concisely: For any function `s` mapping `Prop` to sets of type `α`, the indexed union over `s` at `True` equals `s` applied to the trivial proof of `True`.
|
Set.iUnion₂_subset
theorem Set.iUnion₂_subset :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {t : Set α},
(∀ (i : ι) (j : κ i), s i j ⊆ t) → ⋃ i, ⋃ j, s i j ⊆ t
This theorem states that for any type `α`, any index type `ι`, any dependent type `κ` indexed by `ι`, any family of sets `s` indexed by `ι` and `κ`, and any set `t` of type `α`, if each set `s i j` (for all `i` in `ι` and `j` in `κ i`) is a subset of `t`, then the union over all `i` and `j` of the sets `s i j` is also a subset of `t`. In mathematical terms, if $\forall i \in \text{index set } \text{I}, \forall j \in \text{dependent type } \text{K}_i, s_{i,j} \subseteq t$, then $\bigcup_{i \in \text{I}} \bigcup_{j \in \text{K}_i} s_{i,j} \subseteq t$.
More concisely: If for each index `i` in an index set and each index `j` in the dependent type indexed by `i`, the set `s i j` is a subset of a given set `t`, then the union over all `i` and `j` of `s i j` is also a subset of `t`.
|
Set.preimage_iInter
theorem Set.preimage_iInter :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {s : ι → Set β}, f ⁻¹' ⋂ i, s i = ⋂ i, f ⁻¹' s i := by
sorry
The theorem `Set.preimage_iInter` states that for any types `α` and `β`, any indexing type `ι`, any function `f` from `α` to `β`, and any indexed family of sets `s` of `β`, the preimage (`f⁻¹`) of the intersection of the sets `s i` (for all `i` in `ι`) is equal to the intersection of the preimages of the sets `s i`. In other words, taking the preimage of an intersection of sets under a function coincides with taking the intersection of the preimages of the sets.
More concisely: For any function `f` from type `α` to type `β` and any indexed family `(S : ∀ i, β → Prop)` of sets of `β`, `f⁻¹ (∧ i in ι, S i) = ∧ i in ι, f⁻¹ S i`.
|
Set.iUnion_iInter_subset
theorem Set.iUnion_iInter_subset :
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {s : ι → ι' → Set α}, ⋃ j, ⋂ i, s i j ⊆ ⋂ i, ⋃ j, s i j
This theorem states that for any type `α`, and any two index types `ι` and `ι'`, given a function `s` from `ι` and `ι'` to a set of elements of type `α`, the union over `j` of the intersection over `i` of `s i j` is a subset of the intersection over `i` of the union over `j` of `s i j`. In terms of set theory, this means that if you have a family of sets indexed by two parameters `i` and `j`, the union of the intersections over one index is contained within the intersection of the unions over the other index.
More concisely: For any type `α` and functions `s : ι × ι' → α`, the set-theoretic union over `j` of the set-theoretic intersections over `i` of `s i j` is contained in the set-theoretic intersection over `i` of the set-theoretic unions over `j` of `s i j`.
|
Set.setOf_forall
theorem Set.setOf_forall :
∀ {β : Type u_2} {ι : Sort u_4} (p : ι → β → Prop), {x | ∀ (i : ι), p i x} = ⋂ i, {x | p i x}
This theorem, `Set.setOf_forall`, states that for any given type `β` and a type-indexed proposition `p` on `β`, the set of all elements `x` in `β` that satisfy the proposition `p` for all types `ι` is equal to the intersection of all sets `{x | p i x}` for each type `ι`. In other words, it represents the logical intersection of sets: any element in the intersection of all sets must satisfy the condition for all sets.
More concisely: The set of all elements satisfying a type-indexed proposition for all types is equal to the intersection of the sets of elements satisfying the proposition for each type.
|
Set.iUnion_empty
theorem Set.iUnion_empty : ∀ {α : Type u_1} {ι : Sort u_4}, ⋃ x, ∅ = ∅
This theorem states that for any type `α` and an index type `ι`, the indexed union over an empty set results in an empty set. In mathematical terms, it says that if we take the union of an empty set for any index `x` from an index set `ι`, the result is an empty set. This is a generalization of the fact that the union of zero sets is an empty set.
More concisely: For any index type `ι`, the indexed union over an empty set is an empty set.
|
Mathlib.Data.Set.Lattice._auxLemma.4
theorem Mathlib.Data.Set.Lattice._auxLemma.4 :
∀ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} {t : Set α}, (⋃ i, s i ⊆ t) = ∀ (i : ι), s i ⊆ t
This theorem, from the Mathlib library in Lean 4, states that for any type `α` and any sort `ι`, given a function `s` from `ι` to a set of `α` and a set `t` of `α`, the statement that the union over `i` of `s i` is a subset of `t` is equivalent to the statement that for all `i` in `ι`, `s i` is a subset of `t`. In other words, all the sets `s i` are subsets of `t` if and only if their union is a subset of `t`.
More concisely: For any function from a sort to a set of types and a set, the union of the images of the function equals the set if and only if each image is a subset of the set.
|
Set.mem_iUnion_of_mem
theorem Set.mem_iUnion_of_mem :
∀ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} {a : α} (i : ι), a ∈ s i → a ∈ ⋃ i, s i
The theorem `Set.mem_iUnion_of_mem` states that for any type `α`, any indexing type `ι`, any function `s` from `ι` to a set of `α`, and any element `a` of `α`, if `a` belongs to the set `s i` for some index `i` of type `ι`, then `a` also belongs to the union of all sets `s i` for all `i` in `ι`. In other words, if an element is in any of the sets, it is also in their union.
More concisely: If `α` is a type, `ι` is an indexing type, `s : ι → Set α`, and `a : α`, then `a ∈ ⋃i : ι. s i` whenever there exists an `i : ι` such that `a ∈ s i`.
|
Set.iUnion_iUnion_eq_or_left
theorem Set.iUnion_iUnion_eq_or_left :
∀ {α : Type u_1} {β : Type u_2} {b : β} {p : β → Prop} {s : (x : β) → x = b ∨ p x → Set α},
⋃ x, ⋃ (h : x = b ∨ p x), s x h = s b ⋯ ∪ ⋃ x, ⋃ (h : p x), s x ⋯
This theorem states that for any types `α` and `β`, any element `b` of type `β`, any predicate `p` on `β`, and any family of sets `s` indexed by elements of `β` that satisfy either being equal to `b` or satisfying the predicate `p`, the union over all `x` of `β` of the unions over all proofs `h` that `x` equals `b` or `p` holds for `x` of the sets `s x h`, is equal to the union of the set `s b` with the union over all `x` of `β` of the unions over all proofs `h` that `p` holds for `x` of the sets `s x h`. In other words, the union over all elements and all qualifying predicates is the same as the union of the set for a particular element and all qualifying predicates.
More concisely: For any types `α`, any predicate `p` on `β`, and any family `s` indexed by `β` such that for each `x` in `β` the set `s x` is either equal to `{b}` when `x = b` or a subset of `s b` when `p(x)` holds, the union of `s x h` over all `x` in `β` and all proofs `h` that `x = b` or `p(x)` holds is equal to `s b ∪ ⋃(s x h)` over all `x` in `β` and all proofs `h` that `p(x)` holds.
|
Set.sInter_singleton
theorem Set.sInter_singleton : ∀ {α : Type u_1} (s : Set α), {s}.sInter = s
This theorem states that for any set `s` of type `α`, the intersection over the singleton collection containing just `s` is equal to `s` itself. In mathematical terms, for all sets `s`, the intersection of the elements of the singleton set `{s}` is equal to `s`.
More concisely: For any set `s`, the intersection of the singleton set `{s}` is equal to `s`.
|
Set.biUnion_subset_biUnion_left
theorem Set.biUnion_subset_biUnion_left :
∀ {α : Type u_1} {β : Type u_2} {s s' : Set α} {t : α → Set β}, s ⊆ s' → ⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t x
The theorem `Set.biUnion_subset_biUnion_left` states that for any types `α` and `β`, any two sets `s` and `s'` of type `Set α`, and any function `t` mapping elements of `α` to `Set β`, if `s` is a subset of `s'`, then the union of `t x` for all `x` in `s` is also a subset of the union of `t x` for all `x` in `s'`. In other words, if we have a set of element sets derived from `s`, and `s` is a subset of `s'`, then the derived set from `s` is a subset of the derived set from `s'`.
More concisely: If `s` is a subset of `s'`, then the union of `t(x)` for all `x` in `s` is a subset of the union of `t(x)` for all `x` in `s'`.
|
Set.iInter_subtype
theorem Set.iInter_subtype :
∀ {α : Type u_1} {β : Type u_2} (p : α → Prop) (s : { x // p x } → Set β),
⋂ x, s x = ⋂ x, ⋂ (hx : p x), s ⟨x, hx⟩
This theorem states that for any two types `α` and `β`, and for any predicate `p` acting on elements of `α`, the nested intersection over all the sets `s x`, where `x` is an element of the subtype `{ x // p x }`, is equivalent to the intersection over all elements `x` and for every proof `hx` that `p x` holds, the sets `s { val := x, property := hx }`. In other words, it states that the intersection over sets using elements of a subtype is the same as the intersection over sets using elements and the corresponding proofs of a certain predicate.
More concisely: For any types `α`, predicate `p` on `α`, and subsets `s` indexed by elements `x` in the subtype `{ x // p x },` the intersection of all `s x` is equal to the intersection of all sets `s { x // hx }` for every `x` and proof `hx` of `p x`.
|
Set.iInter₂_subset
theorem Set.iInter₂_subset :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} (i : ι) (j : κ i),
⋂ i, ⋂ j, s i j ⊆ s i j
The theorem `Set.iInter₂_subset` states that for any type `α`, any type-indexed type `κ` indexed by `ι`, and any function `s` mapping an index `i` of type `ι` and an index `j` of type `κ[i]` to a set of elements of type `α`, for any specific indices `i` of type `ι` and `j` of type `κ[i]`, the intersection over all `i` and over all `j` of the sets `s[i][j]` is a subset of the specific set `s[i][j]`. This theorem is a statement about the properties of intersections of indexed families of sets.
More concisely: For any type `α`, type-indexed family `κ` of types, and function `s` mapping `(ι × κ)` to sets of `α`, the indexed intersections of `s` are included in each individual set in the image of `s`.
|
Set.sUnion_powerset_gc
theorem Set.sUnion_powerset_gc : ∀ {α : Type u_1}, GaloisConnection (fun x => x.sUnion) fun x => x.powerset
The theorem `Set.sUnion_powerset_gc` states that for any type `α`, the functions `sUnion` and `powerset` form a Galois connection. In other words, for any pair of sets `a` and `b`, the union of all elements in `a` is a subset of `b` if and only if `a` is a subset of the powerset of `b`. Here, `sUnion` is a function that takes a set of sets and returns the union of all these sets, and `powerset` is a function that takes a set and returns its powerset, which is the set of all its subsets.
More concisely: The `Set.sUnion` and `powerset` functions form a Galois connection, meaning that for any sets `a` and `b`, `sUnion (map (set.subset a) (powerset b)) = b` if and only if `a ⊆ b`.
|
Set.iUnion_union_distrib
theorem Set.iUnion_union_distrib :
∀ {β : Type u_2} {ι : Sort u_4} (s t : ι → Set β), ⋃ i, s i ∪ t i = (⋃ i, s i) ∪ ⋃ i, t i
The theorem `Set.iUnion_union_distrib` states that for any type `β` and any index type `ι`, the distributed union of indexed sets `s` and `t` over all indices `i` is equal to the union of the indexed union of `s` and the indexed union of `t`. In more mathematical terms, it expresses the property that the union over an index set of the union of two sets (each indexed by the same set) is equal to the union of the unions over the index set of the two sets separately. This is the distributive property of union over indexed sets.
More concisely: For any type `β` and index type `ι`, the indexed union of `s ∪ t` over `ι` equals the indexed union of `s` and `t` over `ι`. In other words, `⋃i, σ i. (s i ∪ t i) = ⋃i, σ i. (s i) ∪ (t i)`, where `σ i` denotes the indexed family structure.
|
Set.iUnion_coe_set
theorem Set.iUnion_coe_set :
∀ {α : Type u_11} {β : Type u_12} (s : Set α) (f : ↑s → Set β), ⋃ i, f i = ⋃ i, ⋃ (h : i ∈ s), f ⟨i, h⟩
This theorem states that for any types `α` and `β`, a given set `s` of type `α`, and a function `f` mapping elements of the coerced set `s` to sets of type `β`, the union over all elements of the function `f` is equal to the union over all elements `i` and all properties `h` (where `h` signifies that `i` is an element of `s`) of the function `f` applied to the element `i` with property `h`. In other words, this theorem expresses a property of unions in the context of function application over sets.
More concisely: For any sets `α`, `β`, type `α` set `s`, and function `f` from `s` to sets of type `β`, the set union over `f` is equal to the set union over all elements `i` in `s` and their membership properties `h`, i.e., `⋃(f ↦ x in s) (f x) = ⋃(x : s) (h : x ∈ s) (f x)`.
|
Set.inter_eq_iInter
theorem Set.inter_eq_iInter : ∀ {α : Type u_1} {s₁ s₂ : Set α}, s₁ ∩ s₂ = ⋂ b, bif b then s₁ else s₂
This theorem states that for any type `α` and any two sets `s₁` and `s₂` of type `α`, the intersection of `s₁` and `s₂` is equivalent to the intersection over all `b` such that if `b` is true, then we consider `s₁`, else we consider `s₂`. In other words, the intersection of the two sets `s₁` and `s₂` is the same as the intersection of all elements from either `s₁` or `s₂` depending on whether a certain condition `b` is met.
More concisely: For any type `α` and sets `s₁`, `s₂` of type `α`, the intersection of `s₁` and `s₂` equals the intersection of `s₁` if a condition `b` holds, and the intersection of `s₂` otherwise.
|
Set.iInter_mono
theorem Set.iInter_mono :
∀ {α : Type u_1} {ι : Sort u_4} {s t : ι → Set α}, (∀ (i : ι), s i ⊆ t i) → ⋂ i, s i ⊆ ⋂ i, t i
This theorem states that for any type `α` and any index type `ι`, if we have two indexed families of sets `s` and `t` (both indexed by `ι` and containing sets of type `α`), then if every set in `s` is a subset of the corresponding set in `t` (i.e., for all `i` in `ι`, `s i` is a subset of `t i`), it follows that the intersection over all sets in `s` is a subset of the intersection over all sets in `t`. In terms of set theory, this states that if every element of a collection of sets `s` is subset of the corresponding element in another collection `t`, then the intersection of all elements of `s` is a subset of the intersection of all elements of `t`.
More concisely: If for all indices i, si ⊆ ti, then ∩ gi∈I si = ∩ gi∈I ti. (In set theory, if every set si in an indexed family is a subset of the corresponding set ti, then the intersection of all si is a subset of the intersection of all ti.)
|
Set.compl_iUnion
theorem Set.compl_iUnion : ∀ {β : Type u_2} {ι : Sort u_4} (s : ι → Set β), (⋃ i, s i)ᶜ = ⋂ i, (s i)ᶜ
The theorem `Set.compl_iUnion` states that for any type `β` and any indexing type `ι`, if `s` is a function from `ι` to the set of `β`, then the complement of the union over all `s i` is equal to the intersection of the complements of all `s i`. This is a statement of De Morgan's law for sets. In mathematical notation, it says that $(\bigcup_{i} s_i)^c = \bigcap_{i} (s_i)^c$, where $s_i$ are the sets indexed by `i`, $^c$ denotes set complement, $\bigcup$ denotes union over all sets, and $\bigcap$ denotes intersection over all sets.
More concisely: The complement of the union of a family of sets equals the intersection of their complements.
|
Set.preimage_kernImage
theorem Set.preimage_kernImage :
∀ {α : Type u_1} {β : Type u_2} {f : α → β}, GaloisConnection (Set.preimage f) (Set.kernImage f)
The theorem `Set.preimage_kernImage` states that for any two types `α` and `β`, and any function `f` from `α` to `β`, there exists a Galois connection between the preimage function under `f` and the kernel image function of `f`. In other words, for any two sets `a` and `b`, `a` is a subset of the preimage of `b` under `f` if and only if `b` is a subset of the kernel image of `a` under `f`. This is a relationship between two operations on sets that is similar to adjoint functors in category theory.
More concisely: For any function between types `f : α → β`, the preimage and kernel image functions `f⁁⁻¹` and `f.ker` form a Galois connection, that is, `a ⊆ f⁁⁻¹ b` if and only if `b ⊆ f.ker a`.
|
Set.sUnion_mono
theorem Set.sUnion_mono : ∀ {α : Type u_1} {S T : Set (Set α)}, S ⊆ T → S.sUnion ⊆ T.sUnion
The theorem `Set.sUnion_mono` states that for any type `α` and for any two sets `S` and `T` of sets of type `α`, if `S` is a subset of `T`, then the union of all sets in `S` is also a subset of the union of all sets in `T`. In other words, this theorem establishes that the operation of taking the union of all sets within a given set preserves the subset relation.
More concisely: If `S` is a subset of `T` in the type of sets over `α`, then `⋃(s : Set α | s ∈ S)` is a subset of `⋃(t : Set α | t ∈ T)`.
|