Mathlib.Data.Set.Defs._auxLemma.4
theorem Mathlib.Data.Set.Defs._auxLemma.4 :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, (a ∈ f ⁻¹' s) = (f a ∈ s)
This theorem states that for any types `α` and `β`, for any function `f` from `α` to `β`, for any set `s` of type `β`, and for any element `a` of type `α`, `a` is in the preimage of `s` under `f` if and only if `f(a)` is in `s`. In other words, it says that an element is in the preimage of a set via a function if and only if the image of the element under the function is in the set. This is a fundamental property of the preimage operation in set theory.
More concisely: For any functions f: α → β, set s ⊆ β, and element a ∈ α, a ∈ f⁻¹(s) if and only if f(a) ∈ s. (The preimage of a set under a function is equal to the set of elements mapping to elements in the set.)
|
Set.mem_univ_pi
theorem Set.mem_univ_pi :
∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {f : (i : ι) → α i},
f ∈ Set.univ.pi t ↔ ∀ (i : ι), f i ∈ t i
This theorem, `Set.mem_univ_pi`, states that for any type `ι`, any function `α` mapping elements of `ι` to a type, any family of sets `t` where each set is associated with an element of `ι`, and any function `f` with the same domain and range as `α`, the function `f` is an element of the set of all functions associating elements of `ι` to elements in the corresponding set in `t` if and only if for every element `i` of `ι`, the value `f(i)` belongs to the set `t(i)`. In other words, a function is in the set of all functions generated by `Set.pi` over the universal set and the family `t` if and only if all its values are in the corresponding set from the family `t`.
More concisely: For any type `ι`, function `α: ι → Type`, family of sets `t: ι → Set`, and function `f: ι → ∏ i: ι, t(i)`, `f ∈ ∏ i: ι, t(i) → ι, α(i)` if and only if `α(i) ∈ t(i)` for all `i ∈ ι`.
|
Set.comp_rangeSplitting
theorem Set.comp_rangeSplitting : ∀ {α : Type u} {β : Type v} (f : α → β), f ∘ Set.rangeSplitting f = Subtype.val := by
sorry
The theorem `Set.comp_rangeSplitting` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, the composition of the function `f` with the `rangeSplitting` of `f` is equal to the `Subtype.val` function. In other words, if we first take an element from the range of `f`, find a preimage of it using `rangeSplitting`, and then map it back to the range using `f`, we end up where we started. This formalizes the intuition that `rangeSplitting` chooses a preimage for each element in the range of `f`, and applying `f` to a preimage gives the original element.
More concisely: For all types α and β, and for any function f from α to β, the composition of f with the range splitting of f is equal to the identity function on the image of f.
|
Set.diff_eq
theorem Set.diff_eq : ∀ {α : Type u} (s t : Set α), s \ t = s ∩ tᶜ
This theorem states that for all types `α` and for any two sets `s` and `t` of type `α`, the difference of `s` and `t`, denoted as `s \ t`, is equal to the intersection of `s` and the complement of `t`, denoted as `s ∩ tᶜ`. In other words, the set of all elements in `s` that are not in `t` is the same as the set of all elements in `s` that are in the set of all elements not in `t`.
More concisely: For all types `α` and sets `s` and `t` of type `α`, `s \ t` equals the intersection of `s` and the complement of `t`, denoted `s ∩ tᶜ`.
|
Mathlib.Data.Set.Defs._auxLemma.2
theorem Mathlib.Data.Set.Defs._auxLemma.2 : ∀ {α : Type u} (s : Set α) (x : α), (x ∈ sᶜ) = (x ∉ s)
This theorem states that for any type `α`, any set `s` of type `α`, and any element `x` of type `α`, the statement "x is in the complement of set s" is equivalent to the statement "x is not in set s". Here, the complement of a set `s` (denoted as `sᶜ` in Lean 4) consists of all elements in the universal set (which includes all possible elements of type `α`) that are not in `s`. In mathematical notation, this can be expressed as `x ∈ sᶜ ⟺ x ∉ s`.
More concisely: For any type `α` and set `s` of type `α`, the element `x` is in the complement of `s` if and only if `x` is not in `s`. In Lean 4 notation, `x ∈ sᶜ ↔ x ∉ s`.
|
Set.mem_preimage
theorem Set.mem_preimage : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, a ∈ f ⁻¹' s ↔ f a ∈ s := by
sorry
The theorem `Set.mem_preimage` states that for any types `α` and `β`, any function `f` from `α` to `β`, any set `s` of elements of type `β`, and any element `a` of type `α`, `a` is an element of the preimage of `s` under `f` if and only if `f(a)` is an element of `s`. In other words, it says that an element belongs to the preimage of a set under a function exactly when its image under the function belongs to the original set. This theorem formalizes one of the fundamental properties of the preimage of a set under a function in set theory.
More concisely: For any function between sets, an element is in the preimage if and only if its image is in the given set.
|
Mathlib.Data.Set.Defs._auxLemma.5
theorem Mathlib.Data.Set.Defs._auxLemma.5 :
∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (y : β), (y ∈ f '' s) = ∃ x ∈ s, f x = y
This theorem states that for any types `α` and `β`, a function `f` from `α` to `β`, a set `s` of type `α`, and an element `y` of type `β`, `y` is in the image of set `s` under function `f` if and only if there exists an element `x` in set `s` such that `f` of `x` equals `y`. In other words, the statement is about the definition of the image of a set under a function: the image of `s` under `f` contains `y` exactly when `y` is the `f`-image of some element of `s`.
More concisely: The image of a set under a function is equal to the set of images of elements in the set under that function.
|
Set.mem_prod
theorem Set.mem_prod :
∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β}, p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t
The theorem `Set.mem_prod` states that for any types `α` and `β`, and any sets `s` of type `α` and `t` of type `β`, and any pair `p` of type `(α, β)`, `p` is an element of the Cartesian product of sets `s` and `t` if and only if the first element of `p` is in `s` and the second element of `p` is in `t`. In mathematical terms, this can be represented as `(p ∈ s × t) ⇔ (p.1 ∈ s ∧ p.2 ∈ t)`, where `s × t` denotes the Cartesian product of sets `s` and `t`, `p.1` and `p.2` denote the first and second elements of the pair `p`, and `∈`, `∧`, and `⇔` denote elementhood, logical conjunction (and), and logical equivalence (if and only if), respectively.
More concisely: The theorem `Set.mem_prod` asserts that for any sets `s` and `t` and pair `p`, `p ∈ s × t` if and only if `p.1 ∈ s` and `p.2 ∈ t`.
|
Set.mem_diff
theorem Set.mem_diff : ∀ {α : Type u} {s t : Set α} (x : α), x ∈ s \ t ↔ x ∈ s ∧ x ∉ t
The theorem `Set.mem_diff` states that for any type `α`, and any two sets `s` and `t` of type `α`, an element `x` of type `α` belongs to the difference of `s` and `t` (denoted `s \ t`) if and only if `x` belongs to `s` and `x` does not belong to `t`. Here, the difference of two sets `s` and `t` is the set of elements that are in `s` but not in `t`.
More concisely: For any type `α` and sets `s` and `t` of type `α`, an element `x` belongs to `s \ t` if and only if `x` is in `s` but not in `t`.
|
Mathlib.Data.Set.Defs._auxLemma.3
theorem Mathlib.Data.Set.Defs._auxLemma.3 : ∀ {α : Type u} {s t : Set α} (x : α), (x ∈ s \ t) = (x ∈ s ∧ x ∉ t) := by
sorry
This theorem, named `Mathlib.Data.Set.Defs._auxLemma.3`, states that for all types `α`, and for all sets `s` and `t` of type `α`, for any element `x` of type `α`, the statement "x is in the difference of sets s and t" is equivalent to the statement "x is in set s and x is not in set t". In mathematical notation, this is saying that $x \in (s \setminus t)$ if and only if $x \in s$ and $x \notin t$. The difference of two sets (also called the set-theoretic difference or relative complement) is the set of all elements that are in the first set but not in the second set.
More concisely: For all types `α`, sets `s` and `t` of type `α`, and element `x` of type `α`, $x \in (s \setminus t) \Leftrightarrow x \in s \land x \notin t$.
|
Set.apply_rangeSplitting
theorem Set.apply_rangeSplitting :
∀ {α : Type u} {β : Type v} (f : α → β) (x : ↑(Set.range f)), f (Set.rangeSplitting f x) = ↑x
The theorem `Set.apply_rangeSplitting` states that for any function `f` from a type `α` to a type `β` and any `x` in the range of `f`, applying `f` to the preimage of `x` (obtained using the `Set.rangeSplitting` function on `f` and `x`) results in `x` itself. In other words, it guarantees that `Set.rangeSplitting` correctly identifies a preimage for each element in the range of the function `f`. This is a formal statement of the property that the function `f` reverses when applied to the output of `Set.rangeSplitting`.
More concisely: For any function `f` from type `α` to type `β` and any `x` in the range of `f`, `f (Set.rangeSplitting f x) = x`.
|
Set.mapsTo_preimage
theorem Set.mapsTo_preimage : ∀ {α : Type u} {β : Type v} (f : α → β) (t : Set β), Set.MapsTo f (f ⁻¹' t) t
The theorem `Set.mapsTo_preimage` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, and any set `t` of type `β`, the image of the preimage of `t` under `f` is contained in `t`. In other words, if we take any set `t`, find its preimage under `f`, and then apply `f` to this preimage, all the resulting elements are guaranteed to be in `t`. This can also be expressed as: for all elements `x` in the preimage of `t` under `f`, `f(x)` is in `t`.
More concisely: For all functions $f:\alpha \to \beta$ and sets $t \subseteq \beta$, the image of $f$'s preimage under $t$ is contained in $t$: $f\^{-1}(t) \subseteq t$.
|
Mathlib.Data.Set.Defs._auxLemma.9
theorem Mathlib.Data.Set.Defs._auxLemma.9 :
∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β}, (p ∈ s ×ˢ t) = (p.1 ∈ s ∧ p.2 ∈ t)
This theorem states that for any sets `s` of type `α` and `t` of type `β`, and any ordered pair `p` of type `α × β`, the pair `p` is in the Cartesian product of the sets `s` and `t` (denoted as `s ×ˢ t`) if and only if the first element of the pair `p` is in the set `s` and the second element of `p` is in the set `t`.
More concisely: For any sets `α`, `β`, `s` of type `α`, and `t` of type `β`, the ordered pair `p` belongs to the Cartesian product `s × βt` if and only if its first component `p.1` belongs to `s` and its second component `p.2` belongs to `t`.
|
Set.mem_range
theorem Set.mem_range : ∀ {α : Type u} {ι : Sort u_1} {f : ι → α} {x : α}, x ∈ Set.range f ↔ ∃ y, f y = x
The theorem `Set.mem_range` says that for any type `α` and any sort `ι`, and for any function `f` from `ι` to `α`, and any element `x` of `α`, `x` is in the range of function `f` if and only if there exists an element `y` such that `f(y)` equals `x`. In other words, an element `x` is in the range of a function `f` precisely when `x` is the image of some element under the function `f`.
More concisely: For any function between types, an element is in the range if and only if it is the image of some element under the function.
|
Mathlib.Data.Set.Defs._auxLemma.12
theorem Mathlib.Data.Set.Defs._auxLemma.12 :
∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {f : (i : ι) → α i},
(f ∈ s.pi t) = ∀ i ∈ s, f i ∈ t i
This theorem states that for any index set `ι`, a family of sets `t` indexed by `ι`, a set `s` of indices, and a dependent function `f`, the function `f` is in the set `Set.pi s t` (the set of dependent functions mapped from set `s` to `t`) if and only if for every index `i` in `s`, `f(i)` is in `t(i)`. Essentially, this theorem is clarifying the condition for a function to be an element of a set of functions, defined by `Set.pi`.
More concisely: A function `f` is in the set `Set.pi s t` if and only if for all indices `i` in `s`, `f(i)` is in `t(i)`.
|
Mathlib.Data.Set.Defs._auxLemma.1
theorem Mathlib.Data.Set.Defs._auxLemma.1 : ∀ {α : Type u} (x : α), (x ∈ Set.univ) = True
This theorem states that for any type `α` and any element `x` of type `α`, `x` is an element of the universal set of type `α`. This is always true regardless of the specific type or element. In terms of set theory, this can be seen as the fact that any element of a certain type belongs to the set of all elements of that type.
More concisely: For any type `α` and any element `x` of type `α`, `x` is a member of the type `α`.
|
Mathlib.Data.Set.Defs._auxLemma.11
theorem Mathlib.Data.Set.Defs._auxLemma.11 :
∀ {α : Type u} {x : α × α} {s : Set α}, (x ∈ s.offDiag) = (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2)
This theorem states that for any type `α`, any pair of elements `x` of type `α`, and any set `s` of type `α`, the pair `x` belongs to the off-diagonal of set `s` if and only if both elements of the pair belong to the set `s` and they are not equal to each other. The off-diagonal of a set `s` is defined as the set of all pairs `(a, b)` where `a` and `b` are elements of `s` and `a` is not equal to `b`.
More concisely: For any type `α` and sets `s` of `α`, the off-diagonal of `s` is equal to the set of pairs `(x, y)` where `x, y ∈ s` and `x ≠ y`.
|
Set.seq_eq_image2
theorem Set.seq_eq_image2 :
∀ {α : Type u} {β : Type v} (s : Set (α → β)) (t : Set α), s.seq t = Set.image2 (fun f a => f a) s t
This theorem establishes an equivalence between the sequence of a set of functions `s` and a set `t` and the image of a binary function which is a member of the set of functions `s` applied to an element of the set `t`. More specifically, for any set of functions `s : Set (α → β)` and a set `t : Set α`, the sequence `Set.seq s t` is equivalent to the image `Set.image2 (fun f a => f a) s t`, where `(fun f a => f a)` is the binary function that applies a function `f` to an element `a`. Essentially, this theorem states that the `Set.seq` operation can be expressed as a specific `Set.image2` operation.
More concisely: The sequence of a set of functions `s` applied to a set `t` is equivalent to the image of the function that applies each function in `s` to each element in `t`.
|
Set.mem_image2_of_mem
theorem Set.mem_image2_of_mem :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β},
a ∈ s → b ∈ t → f a b ∈ Set.image2 f s t
The theorem `Set.mem_image2_of_mem` states that for all types `α`, `β`, and `γ`, a binary function `f : α → β → γ`, and sets `s` of type `α` and `t` of type `β`, if an element `a` of type `α` belongs to set `s`, and an element `b` of type `β` belongs to set `t`, then the result of applying the function `f` to `a` and `b`, which is `f a b`, belongs to the image of the function `f` over sets `s` and `t`, denoted as `Set.image2 f s t`. This image is a set in `γ` that consists of all possible values of `f a b` where `a` is in `s` and `b` is in `t`.
More concisely: For all types `α`, `β`, `γ`, function `f : α → β → γ`, sets `s ⊆ α`, and `t ⊆ β`, if `a ∈ s` and `b ∈ t`, then `f a b ∈ Set.image2 f s t`.
|
Mathlib.Data.Set.Defs._auxLemma.13
theorem Mathlib.Data.Set.Defs._auxLemma.13 :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {s : Set α} {t : Set β} {c : γ},
(c ∈ Set.image2 f s t) = ∃ a ∈ s, ∃ b ∈ t, f a b = c
This theorem states that for all types `α`, `β`, and `γ`, and for any binary function `f : α → β → γ`, and any sets `s : Set α` and `t : Set β`, and any element `c : γ`, the membership of `c` in the image of the function `f` applied over sets `s` and `t` is equivalent to the existence of an element `a` in set `s` and an element `b` in set `t` such that the application of function `f` to `a` and `b` results in `c`. In mathematical terms, it says that \(c\) is in the image of \(f\) over sets \(s\) and \(t\) if and only if there exist elements \(a\) in \(s\) and \(b\) in \(t\) such that \(f(a, b) = c\).
More concisely: For all types `α`, `β`, `γ`, sets `s : Set α`, `t : Set β`, function `f : α → β → γ`, and element `c : γ`, `c ∈ image f s t` if and only if there exist `a ∈ s` and `b ∈ t` such that `c = f a b`.
|
Mathlib.Data.Set.Defs._auxLemma.7
theorem Mathlib.Data.Set.Defs._auxLemma.7 :
∀ {α : Type u} {ι : Sort u_1} {f : ι → α} {x : α}, (x ∈ Set.range f) = ∃ y, f y = x
The theorem `Mathlib.Data.Set.Defs._auxLemma.7` states that for any type `α` and sort `ι`, given a function `f` from `ι` to `α` and an element `x` of type `α`, `x` is in the range of `f` if and only if there exists an element `y` of type `ι` such that `f(y) = x`. In other words, an element is in the range of a function if it's the image of some input to the function.
More concisely: For any function from a type to another type, an element is in the range if and only if it is the image of some input element.
|
Set.mapsTo_image
theorem Set.mapsTo_image : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α), Set.MapsTo f s (f '' s)
The theorem `Set.mapsTo_image` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, and any set `s` of type `α`, the function `f` maps elements of set `s` to the image of `s` under `f`. Here, the image of `s` under `f` (denoted as `f '' s` in Lean 4) is the set of all values that `f` takes on when applied to elements of `s`. Therefore, this theorem is expressing a fundamental property of the image of a set under a function: every element in `s` is mapped to a corresponding element in the image of `s` under `f`.
More concisely: For any function `f` and set `s`, `s ⊆ image (f) ` (i.e., all elements of `s` are in the image of `f`).
|
Set.mem_setOf_eq
theorem Set.mem_setOf_eq : ∀ {α : Type u} {x : α} {p : α → Prop}, (x ∈ {y | p y}) = p x
This theorem states that for any type `α`, any element `x` of type `α`, and any predicate `p` over `α`, the statement "`x` belongs to the set of all elements `y` of type `α` for which the predicate `p` holds" is logically equivalent to the statement "the predicate `p` holds for `x`". In other words, the element `x` is in the set defined by the condition `p` if and only if `x` itself satisfies the condition `p`.
More concisely: For any type `α`, element `x` of type `α`, and predicate `p` over `α`, `x` belongs to the set of elements satisfying `p` if and only if `p` holds for `x`.
|
Set.mem_compl_iff
theorem Set.mem_compl_iff : ∀ {α : Type u} (s : Set α) (x : α), x ∈ sᶜ ↔ x ∉ s
This theorem, `Set.mem_compl_iff`, states that for any type `α`, any set `s` of `α`, and any element `x` of `α`, the element `x` is a member of the complement of set `s` (denoted by `sᶜ`) if and only if `x` is not a member of set `s`. In other words, the theorem provides a property of set complementarity in the context of the membership (`∈`) of an element `x`.
More concisely: For any type `α`, set `s` of `α`, and `x` in `α`, `x` belongs to the complement of `s` if and only if `x` is not an element of `s`.
|
Set.mem_image
theorem Set.mem_image : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (y : β), y ∈ f '' s ↔ ∃ x ∈ s, f x = y := by
sorry
This theorem, `Set.mem_image`, states that for all types `α` and `β`, a function `f` mapping from `α` to `β`, a set `s` of type `α`, and an element `y` of type `β`, `y` is in the image of `s` under `f` if and only if there exists an element `x` in `s` such that `f(x)` equals `y`. In other words, an element is in the image of a set under a function if and only if it is the function's output when applied to some element in the set.
More concisely: For any function `f:` X → Y and set `s` ⊆ X, an element `y` ∈ Y is in the image of `s` under `f` if and only if there exists `x` ∈ s such that `f(x) = y`.
|
Set.mk_mem_prod
theorem Set.mk_mem_prod :
∀ {α : Type u} {β : Type v} {a : α} {b : β} {s : Set α} {t : Set β}, a ∈ s → b ∈ t → (a, b) ∈ s ×ˢ t
This theorem states that for any types `α` and `β`, any elements `a` from `α` and `b` from `β`, and any sets `s` of type `α` and `t` of type `β`, if `a` is an element of set `s` and `b` is an element of set `t`, then the pair `(a, b)` is an element of the cartesian product of sets `s` and `t`. In mathematical terms, if $a \in s$ and $b \in t$, then $(a, b) \in s \times t$.
More concisely: For any sets `s` and `t`, and for all `a in s` and `b in t`, `(a, b) in s × t`.
|
Set.mem_univ
theorem Set.mem_univ : ∀ {α : Type u} (x : α), x ∈ Set.univ
The theorem `Set.mem_univ` states that for any type `α` and any element `x` of that type, `x` is a member of the universal set `Set.univ` on type `α`. In other words, every element of any given type is included in the universal set of that type. This aligns with the concept of a universal set in set theory, which contains all possible elements of a given universe.
More concisely: For any type `α` and any `x : α`, `x ∈ Set.univ (α)`.
|
Set.mem_range_self
theorem Set.mem_range_self : ∀ {α : Type u} {ι : Sort u_1} {f : ι → α} (i : ι), f i ∈ Set.range f
This theorem, `Set.mem_range_self`, states that for any type `α`, any sort `ι`, and any function `f` from `ι` to `α`, for any element `i` of `ι`, the image of `i` under the function `f` is in the range of `f`. In other words, the image of any element of the domain of a function is always in the range (set of output values) of that function.
More concisely: For any function `f : ι -> α`, and any `i : ι`, we have `f i in range f`.
|
Set.mem_image_of_mem
theorem Set.mem_image_of_mem : ∀ {α : Type u} {β : Type v} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a := by
sorry
The theorem `Set.mem_image_of_mem` states that for any types `α` and `β`, and any function `f` from `α` to `β`, if an element `x` of type `α` belongs to a set `a` of `α`, then the image of `x` under `f` belongs to the image of set `a` under `f`. In other words, if a certain `x` is an element of a set `a`, then `f(x)` is an element of the set formed by applying function `f` to each element in `a`.
More concisely: For any function `f` and sets `a` and `X`, if `x ∈ a` and `x ∈ X`, then `f(x) ∈ f(a)`.
|