LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Data.Set.Image

`Function.Surjective.preimage_subset_preimage_iff` theorem Function.Surjective.preimage_subset_preimage_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set β}, Function.Surjective f → (f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t) := by sorry The theorem `Function.Surjective.preimage_subset_preimage_iff` states that for any types `α` and `β`, and any function `f` from `α` to `β`, if `f` is surjective, then the preimage of a set `s` under `f` is a subset of the preimage of a set `t` under `f` if and only if `s` is a subset of `t`. Here, a preimage of a set under a function is the set of all elements in the domain that map to any element in the given set. In mathematical terms, if `f` is a surjection from `α` to `β`, then for any sets `s` and `t` of `β`, `f^-1(s) ⊆ f^-1(t)` if and only if `s ⊆ t`. More concisely: For any surjective function $f$ from type $\alpha$ to type $\beta$, the preimage of set $s$ under $f$ is a subset of the preimage of set $t$ if and only if $s$ is a subset of $t$. In symbols, $f^{-1}(s) \subseteq f^{-1}(t) \Leftrightarrow s \subseteq t$.
`Set.exists_eq_const_of_preimage_singleton` theorem Set.exists_eq_const_of_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty β] {f : α → β}, (∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = Set.univ) → ∃ b, f = Function.const α b The theorem `Set.exists_eq_const_of_preimage_singleton` states that for any two types `α` and `β`, given that `β` is nonempty and `f` is a function mapping from `α` to `β`, if the preimage of any singleton set under `f` is either empty or the universal set of `α`, this implies that `f` is actually a constant function. In other words, if every element in `β` maps to either no elements or all elements in `α` under `f`, then there exists an element in `β` such that `f` is the constant function with that element as its constant value. More concisely: If for all singletons `{x} subset β`, the preimage `f⁻¹'{x}` is either empty or equal to `α`, then `f` is a constant function.
`Set.image_univ_of_surjective` theorem Set.image_univ_of_surjective : ∀ {β : Type u_2} {ι : Type u_6} {f : ι → β}, Function.Surjective f → f '' Set.univ = Set.univ The theorem `Set.image_univ_of_surjective` states that for all types `β` and `ι`, and for any function `f` from `ι` to `β`, if `f` is surjective (i.e., each element `b` in `β` is the image of at least one element `a` in `ι` under the function `f`), then the image of the universal set of `ι` under `f` is the universal set of `β`. In other words, applying a surjective function to every element in the universal set of the domain results in the universal set of the codomain. This captures the idea that a surjective function "covers" every element of its target space. More concisely: If `f : ι → β` is a surjective function, then `image f (univ ι) = univ β`.
`Set.preimage_id` theorem Set.preimage_id : ∀ {α : Type u_1} {s : Set α}, id ⁻¹' s = s The theorem `Set.preimage_id` states that for any type `α` and any set `s` of type `α`, the preimage of `s` under the identity function `id` is the same as the set `s` itself. In other words, applying the identity function to each element of the set `s` does not change the set. The preimage of a set under a function is the collection of all elements that are mapped to the set by the function, and the identity function maps each element to itself. Therefore, every element of `s` is in the preimage, and every element of the preimage is in `s`, so the two sets are equal. More concisely: The preimage of a set under the identity function is equal to the set itself.
`Set.image_perm` theorem Set.image_perm : ∀ {α : Type u_1} {s : Set α} {σ : Equiv.Perm α}, {a \| σ a ≠ a} ⊆ s → ⇑σ '' s = s The theorem states that for any set `s` of type `α` and any permutation `σ` (a bijection from `α` to itself), if the only elements of `α` that are not fixed by `σ` (i.e., for which `σ a ≠ a`) are within `s`, then applying the permutation `σ` to `s` doesn't change `s`, meaning that the image of `s` under `σ` (denoted by `⇑σ '' s`) is equal to `s`. In other words, if a permutation only permutes elements within a set, applying that permutation doesn't change the set. More concisely: If a permutation fixes all elements outside of a set and permutes only the elements within that set, then the set is invariant under the permutation.
`Set.image_eq_preimage_of_inverse` theorem Set.image_eq_preimage_of_inverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α}, Function.LeftInverse g f → Function.RightInverse g f → Set.image f = Set.preimage g The theorem `Set.image_eq_preimage_of_inverse` states that for any two types `α` and `β`, and any two functions `f : α → β` and `g : β → α`, if `g` is a left inverse to `f` (meaning, applying `g` after `f` yields the identity function, or `g ∘ f = id`) and `g` is also a right inverse to `f` (meaning, applying `f` after `g` also gives the identity function, or `f ∘ g = id`), then the image of a set under `f` equals the preimage of the same set under `g`. In other words, applying `f` to all elements of a set `s` in `α` yields exactly the same set of `β` elements as those that would be mapped back into `s` by `g`. More concisely: If functions `f : α → β` and `g : β → α` satisfy `g ∘ f = id_α` and `f ∘ g = id_β`, then `f''(S) = g⁻¹''(S)` for any set `S ⊆ α`.
`Mathlib.Data.Set.Image._auxLemma.12` theorem Mathlib.Data.Set.Image._auxLemma.12 : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, (f '' s ⊆ t) = (s ⊆ f ⁻¹' t) This theorem states that for any types `α` and `β`, for any set `s` of type `α`, for any set `t` of type `β`, and for any function `f` from `α` to `β`, the image of `s` through `f` is a subset of `t` if and only if `s` is a subset of the preimage of `t` through `f`. In mathematical notation, we have $f(s) \subseteq t$ if and only if $s \subseteq f^{-1}(t)$. More concisely: For any functions $f: \alpha \to \beta$, sets $s \subseteq \alpha$, and $t \subseteq \beta$, $f(s) \subseteq t$ if and only if $s \subseteq f^{-1}(t)$.
`Set.preimage_univ` theorem Set.preimage_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f ⁻¹' Set.univ = Set.univ This theorem, `Set.preimage_univ`, states that for any two types `α` and `β`, and any function `f` from `α` to `β`, the preimage of the universal set (`Set.univ`) under `f` is also the universal set. In other words, the set of all elements in `α` that map to some element in the universal set of `β` under `f` is simply the universal set of `α`. This makes sense as the universal set of `β` includes all elements of `β`, so every element of `α` will map to some element in it. More concisely: For any type `α` and `β`, and function `f` from `α` to `β`, `f⁁⁻¹(Set.univ β) = Set.univ α`.
`Set.surjective_onto_range` theorem Set.surjective_onto_range : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, Function.Surjective (Set.rangeFactorization f) The theorem `Set.surjective_onto_range` asserts that for any type `α` and any type-indexed collection `ι`, and any function `f` mapping from `ι` to `α`, the function that factors `f` through its range, `Set.rangeFactorization f`, is surjective. In mathematical terms, this means that for any element in the range of `f`, there exists an element in the domain of `f` such that when this element is mapped by `Set.rangeFactorization f`, we obtain the original element from the range. More concisely: For any function $f$ from a type-indexed collection $\ι$ to a type $\alpha$, the factorization of $f$ through its range is a surjection. In other words, for every $y$ in the range of $f$, there exists $x$ in the domain of $f$ such that $f(x) = y$ and $(Set.rangeFactorization~f)(x) = y$.
`Set.image_pair` theorem Set.image_pair : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a b : α), f '' {a, b} = {f a, f b} This theorem states that for any function `f` from type `α` to type `β`, and any two elements `a` and `b` of type `α`, the image of the set `{a, b}` under the function `f` equals the set `{f(a), f(b)}`. In mathematical terms, if we apply a function to each element in a set containing two elements, we get a new set containing the function applied to each of these two elements. More concisely: For any function `f` from type `α` to type `β`, the image of a set with two elements `{a, b}` under `f` is `{f(a), f(b)}`. In mathematical notation: `f({a, b}) = {f(a), f(b)}`.
`Subtype.coe_image_subset` theorem Subtype.coe_image_subset : ∀ {α : Type u_1} (s : Set α) (t : Set ↑s), Subtype.val '' t ⊆ s The theorem `Subtype.coe_image_subset` states that for all types `α`, any set `s` of type `α`, and any set `t` of elements from the subtype derived from `s` (denoted as `↑s`), the image of `t` under the projection function `Subtype.val` (which sends each element of the subtype back to its underlying type `α`) is a subset of the original set `s`. In other words, when you take a subset of the subtype and apply `Subtype.val` to each element, you will only get elements that are in the original set `s`. More concisely: For any type `α`, set `s` of `α`, and subset `t` of the subtype `↑s`, the image of `t` under the projection function `Subtype.val` is contained in the original set `s`. In mathematical notation, `∀ α, ∀ s : set α, t ⊆ {x : α \| x ∈ s} → {x : α \| x ∈ s}`.
`Set.preimage_compl` theorem Set.preimage_compl : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ The theorem `Set.preimage_compl` states that for any types `α` and `β`, a function `f` from `α` to `β`, and a set `s` of type `β`, the preimage of the complement of `s` under `f` is equal to the complement of the preimage of `s` under `f`. In mathematical terms, if $f : α → β$ and $S$ is a subset of $β$, then $f^{-1}(S^c) = (f^{-1}(S))^c$. Here, $f^{-1}(S)$ denotes the preimage of $S$ under $f`, $S^c$ denotes the complement of $S$, and $f^{-1}(S^c)$ and $(f^{-1}(S))^c$ are sets of elements from `α`. More concisely: For any function $f : α → β$ and set $S$ of type $β$, the preimage of the complement of $S$ under $f$ is equal to the complement of the preimage of $S$ under $f$: $f^{-1}(S^c) = (f^{-1}(S))^c$.
`Set.Subsingleton.image` theorem Set.Subsingleton.image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Subsingleton → ∀ (f : α → β), (f '' s).Subsingleton The theorem `Set.Subsingleton.image` states that for any two types `α` and `β`, and a set `s` of elements of type `α`, if `s` is a subsingleton (i.e., it contains at most one element), then for any function `f` from `α` to `β`, the image of `s` under the function `f` (denoted as `f '' s`) is also a subsingleton. In other words, if a set has at most one element, then the image of that set under any function also has at most one element. More concisely: If `s` is a subsingleton set in type `α`, then the image `f '' s` of `s` under any function `f` from `α` to `β` is also a subsingleton.
`Set.image_eq_empty` theorem Set.image_eq_empty : ∀ {α : Type u_6} {β : Type u_7} {f : α → β} {s : Set α}, f '' s = ∅ ↔ s = ∅ This theorem states that for all types `α` and `β`, for all functions `f` from `α` to `β`, and for all sets `s` of type `α`, the image of the set `s` under the function `f` is empty if and only if the set `s` itself is empty. In other words, a function `f` produces an empty set when applied to all elements of another set `s` if and only if the original set `s` is empty. More concisely: For all types `α` and `β`, and for all functions `f` from `α` to `β`, if `s` is a set of type `α`, then `f''s` is empty if and only if `s` is empty.
`Set.image_congr` theorem Set.image_congr : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Set α}, (∀ a ∈ s, f a = g a) → f '' s = g '' s The theorem `Set.image_congr` states that for all types `α` and `β`, and for all functions `f` and `g` from `α` to `β`, and for any set `s` of type `α`, if for every element `a` in the set `s`, `f(a)` equals `g(a)`, then the image of the set `s` under the function `f` is equal to the image of the set `s` under the function `g`. In other words, if two functions agree on all elements of a given set, their images of that set are equal. More concisely: If two functions from a set to a type agree on every element of the set, then they have equal images of the set.
`Set.range_nonempty` theorem Set.range_nonempty : ∀ {α : Type u_1} {ι : Sort u_4} [h : Nonempty ι] (f : ι → α), (Set.range f).Nonempty := by sorry The theorem `Set.range_nonempty` states that for all types `α` and any sort `ι`, given that `ι` is nonempty (i.e., there exists at least one element of type `ι`), for any function `f` from `ι` to `α`, the range of the function `f` is a nonempty set. In other words, there exists at least one element in the set that is an image of some element of `ι` under the function `f`. More concisely: For any nonempty type `ι` and function `f` from `ι` to a type `α`, the range of `f` is a nonempty set.
`Function.Surjective.preimage_injective` theorem Function.Surjective.preimage_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → Function.Injective (Set.preimage f) The theorem `Function.Surjective.preimage_injective` states that for any types `α` and `β` and any function `f` from `α` to `β`, if `f` is surjective (meaning that for each element `b` in `β` there exists an element `a` in `α` such that `f(a) = b`), then the function that gets the preimage of a set under `f` is injective. In other words, if `f` is surjective, then for any two sets `s1` and `s2` of `β`, if `f` maps the same set of `α` to `s1` and `s2` (`f`'s preimage of `s1` and `s2` are the same), then `s1` and `s2` must be the same set. More concisely: If `f` is a surjective function from type `α` to type `β`, then for any sets `s1` and `s2` in `β`, `f⁁¹(s1) = f⁁¹(s2)` implies `s1 = s2`.
`Set.image_injective` theorem Set.image_injective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective (Set.image f) ↔ Function.Injective f The theorem `Set.image_injective` states that for all types `α` and `β`, and a function `f` mapping from `α` to `β`, the function `Set.image f` is injective if and only if the function `f` itself is injective. In other words, a function `f` is injective if and only if the image of any two different sets under `f` are different. This is a bi-directional conditional statement, meaning that each condition implies the other. More concisely: The map `Set.image f : β → Set α` is an injection if and only if the function `f : α → β` is an injection.
`Mathlib.Data.Set.Image._auxLemma.2` theorem Mathlib.Data.Set.Image._auxLemma.2 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a) This theorem states that for any type `α` and any two entities `a` and `b` of type `α`, the proposition that `a` equals `b` is equivalent to the proposition that `b` equals `a`. This is a fundamental property of equality, which asserts that equality is a symmetric relation. In other words, if `a` equals `b`, then `b` also equals `a`. More concisely: For any type `α` and any `a, b : α`, `a = b` is equivalent to `b = a`.
`Set.leftInverse_rangeSplitting` theorem Set.leftInverse_rangeSplitting : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.LeftInverse (Set.rangeFactorization f) (Set.rangeSplitting f) The theorem `Set.leftInverse_rangeSplitting` states that for any function `f` from type `α` to type `β`, the function `Set.rangeFactorization f` is a left inverse to the function `Set.rangeSplitting f`. This means that if you apply `Set.rangeFactorization f` followed by `Set.rangeSplitting f` to any input, you get the same input back, i.e., `(Set.rangeSplitting f) ∘ (Set.rangeFactorization f) = id`. In other words, if you first factor through the range of `f` and then pick a preimage for every element in the range of `f`, you end up where you started. More concisely: For any function `f` from type `α` to type `β`, `Set.rangeSplitting f ∘ Set.rangeFactorization f = id`.
`Set.Nonempty.image` theorem Set.Nonempty.image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {s : Set α}, s.Nonempty → (f '' s).Nonempty The theorem `Set.Nonempty.image` asserts that for all types `α` and `β`, and for any function `f` mapping elements from type `α` to `β`, if a set `s` of type `α` is non-empty (`Set.Nonempty s`), then the image of `s` under the function `f` (defined as `f '' s`) is also non-empty (`Set.Nonempty (f '' s)`). In other words, if we have a function and a set that isn't empty, when we apply this function to all elements in the set, the resulting set of output values is also not empty. More concisely: If `f` is a function from type `α` to type `β` and `s ≠ ∅` is a non-empty set of type `α`, then `f '' s ≠ ∅`.
`Sum.range_eq` theorem Sum.range_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ⊕ β → γ), Set.range f = Set.range (f ∘ Sum.inl) ∪ Set.range (f ∘ Sum.inr) This theorem, `Sum.range_eq`, states that for all types `α`, `β`, and `γ` and a function `f` that maps each element of the sum type `α ⊕ β` to `γ`, the range of `f` is equal to the union of the ranges of `f` composed with `Sum.inl` and `f` composed with `Sum.inr`. In other words, all elements of `γ` that `f` can possibly output, regardless of whether the input is from `α` or `β`, are either in the range of `f` when applied to elements of `α` or in the range of `f` when applied to elements of `β`. More concisely: For any types `α`, `β`, and `γ`, and a function `f : α ⊕ β → γ`, the range of `f` is equal to the union of the ranges of `f ∘ Sum.inl` and `f ∘ Sum.inr`.
`Set.range_quot_mk` theorem Set.range_quot_mk : ∀ {α : Type u_1} (r : α → α → Prop), Set.range (Quot.mk r) = Set.univ The theorem `Set.range_quot_mk` states that for any type `α` and a binary relation `r` on `α`, the range of the function `Quot.mk r`, which creates an equivalence class for `r`, is the universal set. In other words, every element of the universal set can be represented as an equivalence class under the relation `r`. This means that all possible equivalence classes for `r` on `α` cover the entire set of `α`, leaving no element of `α` unrepresented. More concisely: For any type `α` and binary relation `r` on `α`, the range of `Quot.mk r` is the universe `Set α`. In other words, every element of `Set α` can be expressed as an equivalence class under `r`.
`Set.image_subset_range` theorem Set.image_subset_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), f '' s ⊆ Set.range f := by sorry The theorem `Set.image_subset_range` states that for all types `α` and `β`, and for any function `f` from `α` to `β` and any set `s` of type `α`, the image of `s` under `f` is a subset of the range of `f`. In other words, any element of `β` that can be obtained by applying `f` to an element of `s`, can also be obtained by applying `f` to some element of `α`. This theorem formalizes the idea that the image of a set under a function is always contained within the range of the function. More concisely: For any function between types and any set, the image of the set under the function is contained in the range of the function.
`Set.image_inter_subset` theorem Set.image_inter_subset : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), f '' (s ∩ t) ⊆ f '' s ∩ f '' t The theorem `Set.image_inter_subset` states that for any two sets `s` and `t` of elements of some type `α`, and any function `f` from `α` to another type `β`, the image under `f` of the intersection of `s` and `t` is a subset of the intersection of the image under `f` of `s` and the image under `f` of `t`. In mathematical terms, this is saying that for all sets `s` and `t` and function `f`, we have `f(S ∩ T) ⊆ f(S) ∩ f(T)`. More concisely: The image of the intersection of two sets under a function is a subset of the intersection of the images of those sets under that function.
`Set.preimage_eq_iff_eq_image` theorem Set.preimage_eq_iff_eq_image : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Bijective f → ∀ {s : Set β} {t : Set α}, f ⁻¹' s = t ↔ s = f '' t The theorem `Set.preimage_eq_iff_eq_image` states that for all types `α` and `β`, and a function `f` from `α` to `β` that is bijective, for any set `s` of type `β` and set `t` of type `α`, the preimage of `s` under `f` equals `t` if and only if `s` equals the image of `t` under `f`. This is capturing the relationship between the operations of taking preimages and images for a bijective function. In mathematical language, this would be written as: for a bijective function $f: \alpha \rightarrow \beta$, $f^{-1}(S) = T$ if and only if $S = f(T)$. More concisely: For a bijective function $f: \alpha \rightarrow \beta$, the preimage $f^{-1}(S)$ of a set $S \subseteq \beta$ equals the set $T \subseteq \alpha$ if and only if $S$ equals the image $f(T)$ under $f$.
`Set.range_eq_empty_iff` theorem Set.range_eq_empty_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, Set.range f = ∅ ↔ IsEmpty ι The theorem `Set.range_eq_empty_iff` states that for any type `α` and sort `ι`, and a function `f` from `ι` to `α`, the range of the function `f` is equal to the empty set if and only if the sort `ι` is empty. In other words, a function has an empty range if there are no elements in its domain. More concisely: For any function f from a non-empty sort ι to type α, the range of f is empty if and only if ι is empty.
`Set.Sum.elim_range` theorem Set.Sum.elim_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ), Set.range (Sum.elim f g) = Set.range f ∪ Set.range g The theorem `Set.Sum.elim_range` states that for any two types `α` and `β`, and a sort `γ`, given any two functions `f` from `α` to `γ` and `g` from `β` to `γ`, the range of the function `Sum.elim f g` (which is a function defined on the sum type `α ⊕ β` to `γ` by separately applying `f` and `g` on `α` and `β` respectively) is the union of the ranges of `f` and `g`. In other words, every element in the codomain `γ` that is mapped to by `Sum.elim f g` is also mapped to by either `f` or `g` when these functions are considered separately over their individual domains. More concisely: The range of the function `Sum.elim f g` on the sum type `α ⊕ β` is contained in the union of the ranges of `f` over `α` and `g` over `β`.
`Mathlib.Data.Set.Image._auxLemma.11` theorem Mathlib.Data.Set.Image._auxLemma.11 : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, (f '' s).Nonempty = s.Nonempty The theorem `Mathlib.Data.Set.Image._auxLemma.11` states that for any two types `α` and `β`, a function `f` from `α` to `β`, and a set `s` of type `α`, the image of the set `s` under the function `f` is nonempty if and only if the set `s` is nonempty. In other words, a function will produce a nonempty set from another set if and only if the original set has at least one element. More concisely: For any type `α`, set `s` of type `α`, and function `f` from `α` to another type `β`, the image of `s` under `f` is nonempty if and only if `s` is nonempty.
`Set.range_eq_iff` theorem Set.range_eq_iff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), Set.range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b The theorem `Set.range_eq_iff` states that for any two types `α` and `β`, and any function `f` from `α` to `β`, and any set `s` of type `β`, the range of `f` is equal to `s` if and only if every element of `α` when mapped by `f` is in `s`, and for every element in `s`, there exists an element in `α` such that when this element is mapped by `f`, it equals the given element in `s`. In other words, the range of `f` is exactly `s` if all outputs of `f` are in `s` and all elements of `s` can be obtained by applying `f` to some inputs. More concisely: For any function `f` from type `α` to type `β` and set `s` of type `β`, the range of `f` equals `s` if and only if for all `x` in `α`, `f x` is in `s`, and for all `y` in `s`, there exists an `x` in `α` such that `f x = y`.
`Set.image_eq_image` theorem Set.image_eq_image : ∀ {α : Type u_1} {β : Type u_2} {s t : Set α} {f : α → β}, Function.Injective f → (f '' s = f '' t ↔ s = t) := by sorry The theorem `Set.image_eq_image` states that for all types `α` and `β`, for all sets `s` and `t` of type `α`, and for all functions `f` from `α` to `β`, if `f` is injective (meaning that `f` always produces a unique output for each unique input), then the image of `s` under `f` is equal to the image of `t` under `f` if and only if `s` is equal to `t`. In other words, an injective function `f` maps two sets `s` and `t` to the same set of images if and only if `s` and `t` are the same. This theorem establishes the preservation of set equality under the application of an injective function. More concisely: For injective functions between sets, the image of two sets is equal if and only if the sets are equal.
`Set.preimage_preimage` theorem Set.preimage_preimage : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : Set γ}, f ⁻¹' (g ⁻¹' s) = (fun x => g (f x)) ⁻¹' s This theorem, named `Set.preimage_preimage`, describes a property of function composition and preimages in the context of sets. Specifically, for all types `α`, `β`, and `γ`, and for all functions `g : β → γ` and `f : α → β`, and for any set `s` of type `γ`, the preimage of the preimage of `s` under `f` and `g` is equal to the preimage of `s` under the composition of `g` and `f`. In mathematical terms, it states that $f^{-1}(g^{-1}(s)) = (g \circ f)^{-1}(s)$, where $f^{-1}$ and $g^{-1}$ denote the preimages, not the inverse functions. More concisely: For any sets `α`, `β`, `γ`, functions `f : α → β` and `g : β → γ`, and set `s : Set γ`, the preimages of `s` under `f` and `g` commute, i.e., `f⁻¹(g⁻¹(s)) = (g ∘ f)⁻¹(s)`.
`Set.surjective_onto_image` theorem Set.surjective_onto_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Function.Surjective (Set.imageFactorization f s) := by sorry This theorem states that for any types `α` and `β`, any function `f` from `α` to `β`, and any set `s` of type `α`, the function that results from the image factorization of `f` over `s` is surjective. In mathematical terms, this means that for every element in the image of `f` restricted to `s`, there exists an element in the preimage `s` such that the image factorization function applied to this element equals that element in the image. More concisely: For any function `f` from type `α` to type `β` and any set `s` of type `α`, the image factorization of `f` over `s` is a surjection.
`Set.nontrivial_of_preimage` theorem Set.nontrivial_of_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set β), (f ⁻¹' s).Nontrivial → s.Nontrivial This theorem states that for all types `α` and `β`, and a function `f` from `α` to `β`, if `f` is injective (i.e., every element of `α` maps to a unique element of `β`), then for any set `s` of type `β`, if the preimage of `s` under `f` is nontrivial (i.e., contains at least two distinct elements), then `s` itself is also nontrivial. This theorem establishes a relationship between the properties of a set and its preimage under an injective function. More concisely: If `f` is an injective function from type `α` to type `β`, then the preimage of a non-empty set `s` in `β` under `f` is non-empty and consists of distinct elements.
`Set.image_eq_range` theorem Set.image_eq_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), f '' s = Set.range fun x => f ↑x The theorem `Set.image_eq_range` states that for any two types `α` and `β`, any function `f` from `α` to `β`, and any set `s` of type `α`, the image of `s` under `f` is equal to the range of the function that maps each element `x` in `s` to `f` applied to `x`. In more mathematical terms, it says that the set of all values `f(x)` for `x` in `s` is the same as the set of all possible outputs of the function `f` where the domain is restricted to `s`. More concisely: For any function `f` from type `α` to type `β` and any set `s` of type `α`, the image of `s` under `f` equals the range of the function `x ↔→ f x`.
`Function.Surjective.nonempty_preimage` theorem Function.Surjective.nonempty_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → ∀ {s : Set β}, (f ⁻¹' s).Nonempty ↔ s.Nonempty The theorem `Function.Surjective.nonempty_preimage` states that for any types `α` and `β`, and any function `f` from `α` to `β`, if `f` is a surjective function, then for any set `s` of type `β`, the preimage of `s` under `f` is nonempty if and only if `s` is nonempty. In other words, a set `s` has some value if and only if there is some value in `α` that maps to `s` under the function `f`, given that `f` is surjective. The preimage of `s` under `f` is the set of all elements in `α` that `f` maps to an element in `s`. More concisely: If `f` is a surjective function from `α` to `β`, then for every nonempty `s ∈ β`, the preimage `f⁁¹(s)` is nonempty in `α`.
`Set.preimage_const` theorem Set.preimage_const : ∀ {α : Type u_1} {β : Type u_2} (b : β) (s : Set β) [inst : Decidable (b ∈ s)], (fun x => b) ⁻¹' s = if b ∈ s then Set.univ else ∅ This theorem, `Set.preimage_const`, states that for any types `α` and `β`, a value `b` of type `β`, and a set `s` of type `β`, given a decidable instance for `b` belonging to `s`, the preimage of `s` under the constant function mapping to `b` is equal to the universal set if `b` is in `s`, and is equal to the empty set otherwise. In mathematical terms, if `b` is in `s`, all elements of `α` are mapped to `b`, hence the preimage is the universal set. If `b` is not in `s`, no elements of `α` could have been mapped to `b`, hence the preimage is the empty set. More concisely: For any sets `α` and `β`, and a constant function `f : β → α` with image `s ⊆ β` decidable, if `b ∈ s`, then `f⁁⁻¹(s) = α`, and if `b ∉ s`, then `f⁁⁻¹(s) = ∅`.
`Set.image_nonempty` theorem Set.image_nonempty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, (f '' s).Nonempty ↔ s.Nonempty The theorem `Set.image_nonempty` states that for all types `α` and `β`, for any function `f` from `α` to `β`, and any set `s` of type `α`, the image of `s` under `f` is nonempty if and only if `s` itself is nonempty. This means that a function will map a nonempty set to a nonempty set under its operation, and inversely, if the image of a function is nonempty, then the original set must also have been nonempty. More concisely: For all types α and β, and for any function f from α to β, if s is a nonempty set of type α, then the image of s under f is also a nonempty set. Conversely, if the image of s under f is nonempty, then s itself must be nonempty.
`Set.image_congr'` theorem Set.image_congr' : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Set α}, (∀ (x : α), f x = g x) → f '' s = g '' s The theorem `Set.image_congr'` states that for any types `α` and `β`, and for any two functions `f` and `g` from `α` to `β`, along with a set `s` of elements of type `α`, if `f` and `g` are equivalent (i.e., for all elements `x` of type `α`, `f x` equals `g x`), then the image of `s` under `f` is equal to the image of `s` under `g`. In mathematical terms, this is the same as saying that if two functions are equal everywhere, then their action on any particular set is also the same. More concisely: If `f` and `g` are equal functions from `α` to `β`, then `Set.image s f = Set.image s g`.
`Set.image_union` theorem Set.image_union : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), f '' (s ∪ t) = f '' s ∪ f '' t The theorem `Set.image_union` states that for any two sets `s` and `t` of elements of some type `α`, and any function `f` from `α` to another type `β`, the image of the union of sets `s` and `t` under function `f` is equivalent to the union of the individual images of sets `s` and `t` under the same function. In mathematical notation, this is the property that $f(S \cup T) = f(S) \cup f(T)$ where $S$ and $T$ are sets and $f$ is a function. More concisely: The theorem asserts that for sets $S, T \subseteq \alpha$ and function $f : \alpha \to \beta$, $f(S \cup T) = f(S) \cup f(T)$.
`Set.preimage_eq_preimage` theorem Set.preimage_eq_preimage : ∀ {α : Type u_1} {β : Type u_2} {s t : Set α} {f : β → α}, Function.Surjective f → (f ⁻¹' s = f ⁻¹' t ↔ s = t) := by sorry The theorem `Set.preimage_eq_preimage` states that for any types `α` and `β`, sets `s` and `t` of type `α`, and a surjective function `f` from `β` to `α`, the preimage of `s` under `f` is equal to the preimage of `t` under `f` if and only if `s` is equal to `t`. In other words, if `f` is a surjective function, then the equality of the preimages of two sets under `f` implies the equality of the two sets themselves, and vice versa. More concisely: For surjective functions $f:\beta \to \alpha$, the preimages $f^{-1}(s)$ and $f^{-1}(t)$ are equal if and only if sets $s, t \subseteq \alpha$ are equal.
`Set.image_univ` theorem Set.image_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f '' Set.univ = Set.range f The theorem `Set.image_univ` states that for any types `α` and `β`, and any function `f` from `α` to `β`, the image of the universal set (`Set.univ`) under the function `f` is equal to the range of the function `f`. In more formal terms, it means that the set of all outputs of `f` when applied to all elements of `α` (represented by `f '' Set.univ`) is the same as the set of all possible outputs of `f` (represented by `Set.range f`). This theorem essentially formalizes the idea that the range of a function includes every possible output value when the function is applied to every possible input. More concisely: For any function `f` from type `α` to type `β`, `Set.range f = f '' Set.univ`.
`Mathlib.Data.Set.Image._auxLemma.23` theorem Mathlib.Data.Set.Image._auxLemma.23 : ∀ {α : Sort u} {b : α → Sort v} {p : (x : α) → b x → Prop}, (∀ (x : α), ∃ y, p x y) = ∃ f, ∀ (x : α), p x (f x) The theorem states that for any function `p` from pairs `(x, y)`, where `x` is of some type `α` and `y` is of type `b x`, if for every `x` in `α` there exists a `y` such that `p x y` holds, then there exists a function `f` from `α` to `b x` such that for every `x` in `α`, `p x (f x)` holds. In simpler terms, this theorem asserts the equivalence of the existence of an element for each input satisfying a property and the existence of a function encapsulating this relationship. More concisely: If for every `x` in `α`, there exists a `y` of type `b x` such that `p(x, y)` holds, then there exists a function `f` from `α` to `b` such that `p(x, f(x))` holds for all `x` in `α`.
`Function.Injective.preimage_image` theorem Function.Injective.preimage_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), f ⁻¹' (f '' s) = s The theorem `Function.Injective.preimage_image` states that for any types `α` and `β`, and for any function `f` from `α` to `β`, if `f` is injective then the preimage of the image of a set `s` under `f` is equal to `s` itself. In other words, if we apply `f` to every element of a set `s`, and then look at the set of all inputs that could have produced those outputs, we get back `s`. This is a property of injective functions, which are functions where every output is produced by exactly one input. More concisely: If `f: α → β` is an injective function, then `f''(s) = s` for any set `s` in `α`. Here, `f''(s)` denotes the preimage of the image of `s` under `f`.
`Set.range_eq_empty` theorem Set.range_eq_empty : ∀ {α : Type u_1} {ι : Sort u_4} [inst : IsEmpty ι] (f : ι → α), Set.range f = ∅ The theorem `Set.range_eq_empty` states that for any type `α` and any sort `ι`, if `ι` is an empty type (indicated by the `IsEmpty ι` instance), then for any function `f` from `ι` to `α`, the range of `f` (i.e. the set of all outputs of `f`) is the empty set. In other words, if a function has an empty domain, then its range is also empty. More concisely: If `ι` is an empty type, then the range of any function from `ι` to `α` is the empty set.
`Set.image_singleton` theorem Set.image_singleton : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α}, f '' {a} = {f a} This theorem states that for any types `α` and `β` and any function `f` from `α` to `β`, the image under `f` of the singleton set containing only an element `a` from `α` is the singleton set containing only the image of `a` under `f`. In other words, this theorem connects the concepts of function application and set image by showing that applying a function to a single element is the same as finding the image of a singleton set under that function. More concisely: For any types `α` and `β` and function `f` from `α` to `β`, the image of the singleton set {`a`} under `f` is the set {`f a`}.
`Set.range_subset_iff` theorem Set.range_subset_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {s : Set α}, Set.range f ⊆ s ↔ ∀ (y : ι), f y ∈ s The theorem `Set.range_subset_iff` states that for any type `α`, any sort `ι`, any function `f` from `ι` to `α`, and any set `s` of type `α`, the range of the function `f` is a subset of the set `s` if and only if for every element `y` in `ι`, the function applied to `y` (`f y`) is an element of the set `s`. In simpler terms, it shows the equivalence between the claim that all image points of `f` lie in `s` and the claim that for each input `y`, its image `f(y)` is in `s`. More concisely: For any function `f` from a type `ι` to a set `α`, and any set `s ⊆ α`, the range of `f` is a subset of `s` if and only if every image point `y ∈ ι` satisfies `f y ∈ s`.
`Set.image_preimage_inter` theorem Set.image_preimage_inter : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β), f '' (f ⁻¹' t ∩ s) = t ∩ f '' s The theorem `Set.image_preimage_inter` states that for any function `f` mapping elements of type `α` to type `β`, and for any sets `s` of type `α` and `t` of type `β`, the image under `f` of the intersection of the preimage of `t` under `f` and `s` is equal to the intersection of `t` and the image under `f` of `s`. In terms of set theory, this means that applying a function to the intersection of the preimage of a set and another set results in the same set if we first take the intersection of the original set and the image of the second set. More concisely: For any function `f` from type `α` to type `β` and sets `s ⊆ α` and `t ⊆ β`, `f''(s ∩ f⁁¹(t)) = s ∩ f''(s)`. Here, `f''` represents the image of a set under `f`, and `f⁁¹` represents the preimage of a set under `f`.
`Set.isCompl_range_some_none` theorem Set.isCompl_range_some_none : ∀ (α : Type u_6), IsCompl (Set.range some) {none} The theorem `Set.isCompl_range_some_none` states that for any type `α`, the set of all values that can be generated by applying the `some` function (which wraps a value in an `Option` type) is a complement of the set containing only the `none` value (which represents an absence of a value in `Option` type). In other words, the union of these two sets gives the whole set of all `Option α` values, and their intersection is empty. More concisely: The sets of `Option.some α` values and `Option.none` form a complementary pair, i.e., their union equals the whole `Option α` type and their intersection is empty.
`Set.image_inter_preimage` theorem Set.image_inter_preimage : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β), f '' (s ∩ f ⁻¹' t) = f '' s ∩ t The theorem `Set.image_inter_preimage` states that for all types `α` and `β`, and a function `f` from `α` to `β`, the image of the intersection of a set `s` of type `α` and the preimage of a set `t` under `f` is equal to the intersection of the image of `s` under `f` and `t`. In mathematical terms, given a function `f : α → β`, a set `s ⊆ α`, and a set `t ⊆ β`, we have `f(s ∩ f⁻¹(t)) = f(s) ∩ t`. This theorem relates the concepts of image, intersection, and preimage in the context of sets and functions between them. More concisely: For all sets `s ⊆ α` and `t ⊆ β`, and function `f : α → β`, `f(s ∩ f⁻¹(t)) = f(s) ∩ t`.
`Set.isCompl_range_inl_range_inr` theorem Set.isCompl_range_inl_range_inr : ∀ {α : Type u_1} {β : Type u_2}, IsCompl (Set.range Sum.inl) (Set.range Sum.inr) The theorem `Set.isCompl_range_inl_range_inr` states that for all types `α` and `β`, the range of the function `Sum.inl` (which sends an element from type `α` to the corresponding element in the sum type `α + β`) and the range of the function `Sum.inr` (which sends an element from type `β` to the corresponding element in the sum type `α + β`) are complements of each other in the set of all possible values of the sum type `α + β`. In other words, every element in `α + β` can be uniquely identified as coming from `α` via `Sum.inl` or from `β` via `Sum.inr`, but not both. More concisely: For all types `α` and `β`, the ranges of `Sum.inl` and `Sum.inr` over `α + β` form a pair of complementary subsets, i.e., for all `x : α + β`, `Sum.inl x ∈ Set.range (Sum.inl : α → α + β)` if and only if `Sum.inr x ∉ Set.range (Sum.inr : β → α + β)`.
`Function.Injective.mem_set_image` theorem Function.Injective.mem_set_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ {s : Set α} {a : α}, f a ∈ f '' s ↔ a ∈ s This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β` that is injective, for any set `s` of type `α` and any element `a` of type `α`, the image of `a` under the function `f` is in the image set of `s` under `f` if and only if `a` is in `s`. In other words, an element's image belongs to the image set of given set if and only if the element belongs to the original set, when the function used to form the image set is injective. More concisely: For any injective function `f` and sets `s` of type `α`, an element `a` of type `α` belongs to the image set of `s` under `f` if and only if `f(a)` belongs to the image set of `s` under `f`.
`Set.nonempty_image_iff` theorem Set.nonempty_image_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, (f '' s).Nonempty ↔ s.Nonempty The theorem `Set.nonempty_image_iff` expresses a bi-directional relationship between the non-emptiness of a set and the non-emptiness of its image under a function. More specifically, given any two types `α` and `β`, a function `f` from `α` to `β`, and a set `s` of type `α`, the image of `s` under `f` (denoted as `f '' s`) is non-empty if and only if `s` is non-empty. This means that a set has at least one element if and only if its image under the function also has at least one element. More concisely: For any function between two types and any set, the image of a non-empty set is a non-empty set.
`Set.Nonempty.of_image` theorem Set.Nonempty.of_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, (f '' s).Nonempty → s.Nonempty The theorem `Set.Nonempty.of_image` states that for any types `α` and `β`, a function `f` from `α` to `β`, and a set `s` of type `α`, if the image set of `s` through `f` is nonempty, then the original set `s` is also nonempty. In other words, if there exists at least one element in the image of `s` under `f`, there must exist at least one element in `s` itself. More concisely: If `f` is a function from a nonempty set `α` to a set `β` and the image of a set `s subseteq α` under `f` is nonempty, then `s` is nonempty.
`Set.powerset_insert` theorem Set.powerset_insert : ∀ {α : Type u_1} (s : Set α) (a : α), (insert a s).powerset = s.powerset ∪ insert a '' s.powerset The theorem `Set.powerset_insert` states that for any set `s` of type `α` and any element `a` of type `α`, the powerset of the union of `{a}` and `s` is equal to the union of the powerset of `s` and the set of all sets of the form `{a} ∪ t` for each `t` in the powerset of `s`. Here, the powerset of a set is the set of all subsets of that set, and `''` denotes the image of a set under a function (in this case, the function that inserts `a` into each subset of `s`). More concisely: The powerset of the union of a set and its singular element is equal to the union of the powerset of that set and the sets of the form {singular element} ∪ t, for each t in the powerset of that set.
`Set.preimage_inter` theorem Set.preimage_inter : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set β}, f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t The theorem `Set.preimage_inter` states that, for all types `α` and `β`, a function `f` from `α` to `β`, and any two sets `s` and `t` of `β`, the preimage of the intersection of `s` and `t` under `f` is the same as the intersection of the preimages of `s` and `t` under `f`. In other words, if we have a function `f` and two sets `s` and `t`, then the elements in `α` that `f` maps to both `s` and `t` are the same as the elements that `f` maps to `s` and also the elements that `f` maps to `t`. More concisely: For all types `α` and `β`, functions `f` from `α` to `β`, and sets `s` and `t` of `β`, `f⁻¹(s ∩ t) = f⁻¹(s) ∩ f⁻¹(t)`.
`Set.image_subset_image_iff` theorem Set.image_subset_image_iff : ∀ {α : Type u_1} {β : Type u_2} {s t : Set α} {f : α → β}, Function.Injective f → (f '' s ⊆ f '' t ↔ s ⊆ t) := by sorry This theorem states that for any two sets `s` and `t` of elements of type `α`, and any function `f` from `α` to `β`, if `f` is injective (meaning that it never maps different inputs to the same output), then the image of `s` under `f` is a subset of the image of `t` under `f` if and only if `s` is a subset of `t`. Here, the image of a set under a function is the set of all outputs of that function when applied to elements of the set. Thus, this theorem relates the subset relation on the original sets with the subset relation on their images under an injective function. More concisely: If `f` is an injective function from type `α` to type `β`, then `s ⊆ t` implies `f(s) ⊆ f(t)` and conversely.
`Set.image_inter` theorem Set.image_inter : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α}, Function.Injective f → f '' (s ∩ t) = f '' s ∩ f '' t The theorem `Set.image_inter` asserts that for any two sets `s` and `t` of some type `α` and any injective function `f` from `α` to another type `β`, the image of the intersection of `s` and `t` under `f` is equal to the intersection of the images of `s` and `t` under `f`. In other words, if we apply an injective function `f` to each element in the intersection of `s` and `t`, we get the same result as if we first applied `f` to each element in `s` and `t` individually and then took the intersection. This theorem exemplifies one of the properties of injective functions in the context of set theory. More concisely: For injective functions `f` from set `α` to type `β`, `f''(s ∩ t) = f''(s) ∩ f''(t)`, where `s` and `t` are subsets of `α` and `f''` denotes the image of `α` under `f`.
`Function.Injective.preimage_surjective` theorem Function.Injective.preimage_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Function.Surjective (Set.preimage f) The theorem `Function.Injective.preimage_surjective` states that for any types `α` and `β` and any function `f` from `α` to `β`, if `f` is injective (meaning that if `f x = f y` then `x = y`), then the function mapping each set of `β` elements to its preimage under `f` is surjective. In other words, every set of `α` elements is the preimage under `f` of some set of `β` elements. This can be read as "the preimage operation is surjective for any injective function." More concisely: If `f` is an injective function from type `α` to type `β`, then the preimage function ` f ⁁⁃¹` from `β` to `α` is surjective.
`Set.image_preimage_eq` theorem Set.image_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} (s : Set β), Function.Surjective f → f '' (f ⁻¹' s) = s The theorem `Set.image_preimage_eq` states that for any types `α` and `β`, and any function `f : α → β`, given a set `s` of type `β`, if the function `f` is surjective (i.e., every element of `β` is mapped to by some element of `α`), then the image of the preimage of `s` under `f` is equal to `s`. In other words, if we take all the elements of `α` that `f` maps into `s`, and then apply `f` to these elements, we get back exactly the set `s`. This is a fundamental property of surjective functions. More concisely: If `f : α → β` is surjective, then `f''(∫x : α, f x ∈ s) = s`, where `s ⊆ β` and `∫` denotes the set of elements of `α` mapping to `s` under `f`.
`Function.Surjective.range_eq` theorem Function.Surjective.range_eq : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, Function.Surjective f → Set.range f = Set.univ The theorem `Function.Surjective.range_eq` states that for any function `f` from a type `ι` to another type `α`, if the function `f` is surjective (meaning that for every element `b` in `α`, there is some element `a` in `ι` such that `f(a) = b`), then the range of `f` (i.e., the set of all values that `f` can produce) is equal to the universal set `Set.univ` of `α`, which contains all elements of `α`. In other words, a surjective function's output includes every possible element of the codomain. More concisely: If `f` is a surjective function from type `ι` to type `α`, then the range of `f` equals the universe `Set.univ` of `α`.
`Set.preimage_image_eq` theorem Set.preimage_image_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} (s : Set α), Function.Injective f → f ⁻¹' (f '' s) = s The theorem `Set.preimage_image_eq` asserts that for any set `s` of type `α` and an injective function `f` from `α` to another type `β`, the preimage of the image of `s` under `f` equals to the set `s` itself. In other words, if you apply `f` to each element of `s`, and then find all the elements in the domain that map to these image elements under `f`, you get back the original set `s`. Note that this is true only because `f` is injective, meaning that each element in the domain `α` maps to a unique element in the codomain `β`. In terms of sets, this can be written as $f^{-1}(f(s)) = s$ for injective `f`. More concisely: For an injective function $f$ from a set $S$ to another set, the preimage of the image of $S$ under $f$ equals $S$. In symbols, $f^{-1}(f(S)) = S$.
`Set.range_comp_subset_range` theorem Set.range_comp_subset_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ), Set.range (g ∘ f) ⊆ Set.range g The theorem `Set.range_comp_subset_range` states that for all types `α`, `β`, and `γ` and for any two functions `f` from `α` to `β` and `g` from `β` to `γ`, the range of the composition of `g` and `f` (denoted as `g ∘ f`) is a subset of the range of `g`. This means every element of the set that is the output of the composite function `g ∘ f` is also an element of the set that is the output of the function `g`. More concisely: For all types α, β, γ and functions f : α → β and g : β → γ, the range of their composition g ∘ f is a subset of the range of g. In mathematical notation, range(g ∘ f) ⊆ range(g).
`Set.nontrivial_of_image` theorem Set.nontrivial_of_image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), (f '' s).Nontrivial → s.Nontrivial The theorem states that for any two types `α` and `β`, and a function `f` from `α` to `β`, if the image of a set `s` under the function `f` is nontrivial (i.e., contains at least two distinct elements), then the original set `s` itself is also nontrivial. This property holds for all sets `s` of type `α`. More concisely: If `f` is a function from type `α` to type `β` and the image of a set `s` under `f` contains at least two distinct elements, then set `s` itself contains at least two distinct elements.
`Set.range_iff_surjective` theorem Set.range_iff_surjective : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, Set.range f = Set.univ ↔ Function.Surjective f The theorem `Set.range_iff_surjective` states that for all types `α` and `ι` and a function `f` from `ι` to `α`, the range of `f` equals the universal set of `α` if and only if the function `f` is surjective. In other words, a function `f` is surjective, i.e., for every element `b` of `α` there exists an element `a` in `ι` such that `f(a) = b`, if and only if the set of all values that `f` can take (the range of `f`) is the entire set `α`. More concisely: A function from type `ι` to type `α` is surjective if and only if its range equals the entire set `α`.
`Set.image_diff` theorem Set.image_diff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s t : Set α), f '' (s \ t) = f '' s \ f '' t The theorem `Set.image_diff` states that for all types `α` and `β`, and for an injective function `f` from `α` to `β`, the image of the difference of two sets `s` and `t` (of type `α`) under the function `f` is equal to the difference of the image of `s` under `f` and the image of `t` under `f`. In mathematical terms, this theorem represents the property that for injective functions, the image of the set difference is equal to the difference of the images: $f(S \setminus T) = f(S) \setminus f(T)$. More concisely: For injective functions $f$ from type $\alpha$ to type $\beta$, $f(s \setminus t) = f(s) \setminus f(t)$, where $s$ and $t$ are sets of type $\alpha$.
`Set.rightInverse_rangeSplitting` theorem Set.rightInverse_rangeSplitting : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Function.RightInverse (Set.rangeFactorization f) (Set.rangeSplitting f) The theorem `Set.rightInverse_rangeSplitting` states that for any types `α` and `β`, and any injective function `f` from `α` to `β`, the function `Set.rangeFactorization f` has a right inverse given by the function `Set.rangeSplitting f`. In other words, if you first apply `Set.rangeFactorization f` and then `Set.rangeSplitting f`, you get back the original element. This is equivalent to saying `Set.rangeSplitting f ∘ Set.rangeFactorization f = id`, where `id` is the identity function. More concisely: For any injective function `f` from type `α` to type `β`, `Set.rangeSplitting f ∘ Set.rangeFactorization f = id`.
`Set.image_comp` theorem Set.image_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α → β) (a : Set α), f ∘ g '' a = f '' (g '' a) := by sorry The theorem `Set.image_comp` states that for all types `α`, `β`, and `γ`, and for all functions `f : β → γ` and `g : α → β`, and a set `a` of type `α`, the image of the composition of `f` and `g` on the set `a` is equal to the image of `f` on the image of `g` on the set `a`. In mathematical terms, this theorem is about the associativity of function composition and image generation: $(f \circ g)(A) = f(g(A))$ where $f : \beta \rightarrow \gamma$, $g : \alpha \rightarrow \beta$, and $A$ is a set of type $\alpha$. More concisely: For all sets `α`, `β`, `γ`, functions `f : β → γ` and `g : α → β`, and sets `a : α`, the image of `f` composed with `g` on the set `a` equals the image of `f` applied to the image of `g` on `a`. In mathematical notation: `(∘)<^> image g a = image (f ∘ g) a`.
`Set.subset_preimage_univ` theorem Set.subset_preimage_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, s ⊆ f ⁻¹' Set.univ := by sorry The theorem `Set.subset_preimage_univ` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any set `s` of `α`, the set `s` is a subset of the preimage of the universal set `Set.univ` under the function `f`. In other words, every element of `s` is mapped to some element in the universal set `Set.univ` by the function `f`. More concisely: For any types α and β, function f from α to β, and set s of α, s ⊆ f⁁¹(Set.univ).
`Set.image_preimage_eq_range_inter` theorem Set.image_preimage_eq_range_inter : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {t : Set β}, f '' (f ⁻¹' t) = Set.range f ∩ t This theorem states that for any two types `α` and `β`, and any function `f` from `α` to `β`, the image of the preimage of a set `t` under function `f` is equal to the intersection of the range of function `f` and the set `t`. In mathematical terms, for a set `t` in `β` and a function `f: α → β`, the image of the inverse image of `t` under `f` is the same as the intersection of the range of `f` and `t`. This theorem essentially relates the concepts of function range, image, preimage, and set intersection in a specific way. More concisely: For any function `f: α → β` and set `t ∈ β`, the image of the preimage `f⁁⁻¹(t)` equals the intersection of the range `range(f)` and `t`. In symbols: `f⁁⁻¹(t) = {x : α \| ∃ y : β. x ∈ f⁁⁻¹(y) ∧ y ∈ t} = {x : α \| f(x) ∈ t}`.
`Set.Nonempty.image_const` theorem Set.Nonempty.image_const : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Nonempty → ∀ (a : β), (fun x => a) '' s = {a} The theorem `Set.Nonempty.image_const` states that for any nonempty set `s` of type `α` and any element `a` of type `β`, the image of `s` under the constant function that maps every element to `a` is the singleton set `{a}`. In other words, if you have a nonempty set, and you apply a function to every element in that set where the function always outputs the same value `a`, then the resulting set contains just the one unique element `a`. More concisely: For any nonempty set `s` and element `a`, the image of `s` under the constant function mapping to `a` is the singleton set `{a}`.
`Set.preimage_id'` theorem Set.preimage_id' : ∀ {α : Type u_1} {s : Set α}, (fun x => x) ⁻¹' s = s The theorem `Set.preimage_id'` states that for all sets `s` of any type `α`, the preimage of the set `s` under the identity function is the set `s` itself. In other words, if we apply the identity function to each element of the set `s` and collect the results, we end up with the same set `s`. This is a generalization of the well-known mathematical truth that the identity function leaves all elements unchanged. More concisely: For any set `s` and type `α`, the preimage of `s` under the identity function is equal to `s`.
`Set.image_preimage_eq_inter_range` theorem Set.image_preimage_eq_inter_range : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {t : Set β}, f '' (f ⁻¹' t) = t ∩ Set.range f This theorem asserts that for any types `α` and `β`, and any function `f` from `α` to `β`, and any set `t` of `β`, the image under `f` of the preimage of `t` under `f` equals the intersection of `t` and the range of `f`. In other words, the set of all images under `f` of elements that map to `t` when `f` is applied, coincides with the set of elements that are both in `t` and in the range of `f`. More concisely: For any function `f` from type `α` to type `β` and any subset `t` of `β`, the image of the inverse image of `t` under `f` equals the intersection of `t` and the range of `f`.
`Set.preimage_empty` theorem Set.preimage_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f ⁻¹' ∅ = ∅ This theorem states that for any function `f` from a type `α` to another type `β`, the preimage of an empty set under this function is also an empty set. In mathematical terms, given a function `f: α → β`, if you try to find elements in `α` that `f` maps to an empty set, you will end up with an empty set. More concisely: For any function `f: α → β`, the preimage `f⁁⁻¹(∅)` of the empty set under `f` is an empty set.
`Subtype.image_preimage_coe` theorem Subtype.image_preimage_coe : ∀ {α : Type u_1} (s t : Set α), Subtype.val '' (Subtype.val ⁻¹' t) = s ∩ t := by sorry The theorem `Subtype.image_preimage_coe` states that for any types `α` and any sets `s` and `t` of type `α`, the image of the preimage of `t` under the function `Subtype.val` is equal to the intersection of `s` and `t`. In other words, if we first map elements from `s` to their corresponding elements in `t` using `Subtype.val`, and then map these elements back to their preimages in `s`, the resulting set is exactly the same as the intersection of `s` and `t`. This theorem is a statement about how the operations of taking an image and a preimage commute with taking an intersection of sets. More concisely: For any types `α` and sets `s` and `t` of type `α`, `Subtype.val⁡''(s ∩ t) = s ∩ Subtype.image Subtype.val s t`.
`Subtype.coe_preimage_self` theorem Subtype.coe_preimage_self : ∀ {α : Type u_1} (s : Set α), Subtype.val ⁻¹' s = Set.univ The theorem `Subtype.coe_preimage_self` states that for any set `s` of a type `α`, the preimage of `s` under the function `Subtype.val` (which maps each subtype to its underlying base type element) is the universal set. In other words, for all elements in the universal set, their corresponding `Subtype.val` exist in the original set `s`. More concisely: For any subtype `s : Set α`, the image of `s` under the function `Subtype.val` is equal to the universe `α`.
`Set.range_id` theorem Set.range_id : ∀ {α : Type u_1}, Set.range id = Set.univ This theorem declares that for any type `α`, the range of the identity function (`id`) is the universal set. In other words, if you apply the identity function to all elements of the type `α`, you get all possible elements of that type, forming the universal set, hence covering the whole set of `α`. In mathematical terms, for any `α`, we have $\text{range}(id) = \text{univ}$, where `id` is the identity function. More concisely: For any type `α`, the range of the identity function `id` over `α` equals the universal set, that is, `range(id) = Δα`.
`Set.image_swap_eq_preimage_swap` theorem Set.image_swap_eq_preimage_swap : ∀ {α : Type u_1} {β : Type u_2}, Set.image Prod.swap = Set.preimage Prod.swap This theorem states that for any two types `α` and `β`, the image of a set under the function `Prod.swap` is equal to the preimage under the same function `Prod.swap`. In other words, swapping the elements of ordered pairs in a set is equivalent to looking at the set of elements that, when swapped, would fall in the original set. This establishes a relationship between the `Set.image` and `Set.preimage` functions when the `Prod.swap` function is applied. More concisely: For any set `S` in the product type `α × β`, the sets `Set.image (Prod.swap) S` and `Set.preimage (Prod.swap) S` are equal.
`Set.preimage_singleton_true` theorem Set.preimage_singleton_true : ∀ {α : Type u_1} (p : α → Prop), p ⁻¹' {True} = {a \| p a} This theorem, `Set.preimage_singleton_true`, states that for all types `α`, and for any predicate `p` on `α`, the preimage of the singleton set containing only `True` under `p` is equal to the set of all elements `a` in type `α` for which `p a` holds true. In other words, it's the set of all elements that satisfy the predicate `p`. The preimage under a function of a set is defined to be all the elements that get mapped to any element of that set by the function, so this theorem says that all elements that get mapped to `True` by `p` are exactly those that satisfy `p`. More concisely: For any type `α` and predicate `p` on `α`, the preimage of the singleton set {True} under `p` equals the set of elements `a` in `α` such that `p a` holds true.
`Subtype.image_preimage_val` theorem Subtype.image_preimage_val : ∀ {α : Type u_1} (s t : Set α), Subtype.val '' (Subtype.val ⁻¹' t) = s ∩ t := by sorry This theorem states that for any two sets `s` and `t` of a certain type `α`, the image of the preimage of `t` under the function `Subtype.val` is equal to the intersection of `s` and `t`. In other words, if we first find all elements in a subtype whose corresponding elements in `t` satisfy a specific property, and then map these elements back to their original values, we end up with the intersection of the sets `s` and `t`. Here, `Subtype.val` is a function that takes a subtype and returns its underlying element. More concisely: For any sets `s` and `t` of type `α`, the image of `s.subtype.map Subtype.val` equals the intersection of `s` and `t`.
`Set.preimage_const_of_mem` theorem Set.preimage_const_of_mem : ∀ {α : Type u_1} {β : Type u_2} {b : β} {s : Set β}, b ∈ s → (fun x => b) ⁻¹' s = Set.univ The theorem `Set.preimage_const_of_mem` states that for any types `α` and `β`, for any element `b` of type `β`, and for any set `s` of type `β`, if `b` is an element of `s`, then the preimage of the set `s` under the constant function that maps each element of `α` to `b` is the universal set of `α`. In simple terms, since all elements of `α` map to `b` (and `b` belongs to `s`), all elements of `α` are in the preimage of `s`. More concisely: If `b` is an element of set `s` in type `β`, then the preimage of `s` under the constant function from `α` to `b` is the universal set of `α`.
`Function.Surjective.range_comp` theorem Function.Surjective.range_comp : ∀ {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} {f : ι → ι'}, Function.Surjective f → ∀ (g : ι' → α), Set.range (g ∘ f) = Set.range g The theorem `Function.Surjective.range_comp` states that for any types `α`, `ι`, and `ι'`, and for any function `f` from `ι` to `ι'`, if `f` is surjective, then for any function `g` from `ι'` to `α`, the range of the composition of `g` and `f` is equal to the range of `g`. In simpler terms, if every element in `ι'` comes from applying `f` to some element in `ι`, then applying `g` afterwards doesn't lead to any new elements that weren't in the range of `g` alone. More concisely: If `f: ι → ι'` is surjective and `g: ι' → α` is any function, then `range (g ∘ f) = range g`.
`Set.preimage_inl_image_inr` theorem Set.preimage_inl_image_inr : ∀ {α : Type u_1} {β : Type u_2} (s : Set β), Sum.inl ⁻¹' (Sum.inr '' s) = ∅ := by sorry The theorem `Set.preimage_inl_image_inr` states that for any set `s` of type `β`, the preimage of the image of `s` under the `Sum.inr` function with respect to the `Sum.inl` function is the empty set. In other words, there are no elements in any set of type `α` that, when the `Sum.inl` function is applied, result in an element in the image of `s` under `Sum.inr`. This is essentially saying that there is no overlap between the sets `Sum.inl α` and `Sum.inr s`. More concisely: For any set `s` of type `β`, the preimage of `Sum.image (Sum.inr : α × β → β) s` under `Sum.inl : α × β → α` is the empty set.
`Set.range_inl_union_range_inr` theorem Set.range_inl_union_range_inr : ∀ {α : Type u_1} {β : Type u_2}, Set.range Sum.inl ∪ Set.range Sum.inr = Set.univ This theorem states that for any two types `α` and `β`, the union of the ranges of the functions `Sum.inl` and `Sum.inr`, which separately map each type into the sum type `α ⊕ β`, equals the universal set over the sum type `α ⊕ β`. In other words, every element in the sum type can be obtained either from an element of `α` using `Sum.inl` or from an element of `β` using `Sum.inr`. More concisely: For any types `α` and `β`, the ranges of `Sum.inl` from `α` and `Sum.inr` from `β` cover the entire sum type `α ⊕ β`.
`Set.ball_image_iff` theorem Set.ball_image_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {p : β → Prop}, (∀ y ∈ f '' s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x) This theorem, `Set.ball_image_iff`, states that for any types `α` and `β`, any function `f` from `α` to `β`, any set `s` of type `α`, and any property `p` applicable to elements of type `β`, the following two statements are equivalent: firstly, the property `p` holds for all elements `y` in the image of `s` under `f`; and secondly, for any element `x` in `s`, the property `p` holds for `f(x)`. In other words, it asserts that checking a property on all elements of the image of a set under a function is the same as checking the property on the function's output for all elements of the original set. More concisely: For any functions $f: \alpha \to \beta$, sets $s \subseteq \alpha$, and property $p$ on $\beta$, $p$ holds for all images of $s$ under $f$ if and only if $p$ holds for $f(x)$ for all $x \in s$.
`Set.image_id'` theorem Set.image_id' : ∀ {α : Type u_1} (s : Set α), (fun x => x) '' s = s This theorem, `Set.image_id'`, states that for any set `s` of type `α`, the image of `s` under the identity function (i.e., the function that returns each element `x` as it is) is `s` itself. In other words, applying the identity function to each element of a set doesn't change the set. This theorem is a variant of `image_id`. More concisely: For any set `s`, the image of `s` under the identity function is equal to `s`.
`Set.image_image` theorem Set.image_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (s : Set α), g '' (f '' s) = (fun x => g (f x)) '' s This theorem, referred to as `Set.image_image`, states that for any three types `α`, `β`, and `γ`, and any two functions `f` from `α` to `β` and `g` from `β` to `γ`, and a set `s` of type `α`, the image of the image of `s` under `f` and then `g` is equal to the image of `s` under the composition of `g` and `f`. In other words, applying `f` to each element of `s` and then `g` to the result is the same as applying the composition of `g` and `f` to each element of `s`. This theorem is a variant of `image_comp` and is useful for rewriting expressions in Lean 4. More concisely: For any sets `α, β, γ`, functions `f : α → β` and `g : β → γ`, and set `s ⊆ α`, `image (image s f) g = image s (g ∘ f)`.
`Set.ball_image_of_ball` theorem Set.ball_image_of_ball : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {p : β → Prop}, (∀ ⦃x : α⦄, x ∈ s → p (f x)) → ∀ y ∈ f '' s, p y The theorem `Set.ball_image_of_ball` states that for any types `α` and `β`, any function `f` from `α` to `β`, any set `s` of elements of type `α`, and any predicate `p` on elements of type `β`, if for all elements `x` in the set `s`, the predicate `p` holds for `f(x)`, then for any `y` in the image of `s` under `f`, `p(y)` also holds. In other words, if all elements of a set satisfy a predicate when transformed by a function, then all elements in the image of the set under the function satisfy the predicate. More concisely: If a function maps every element of a set to an element satisfying a predicate, then every image of the set under the function also satisfies the predicate.
`Set.image_comm` theorem Set.image_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {β' : Type u_6} {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ}, (∀ (a : α), f (g a) = g' (f' a)) → f '' (g '' s) = g' '' (f' '' s) The theorem `Set.image_comm` states that for all types `α, β, γ, β'`, and for all sets `s` of type `α`, and for all functions `f` from `β` to `γ`, `g` from `α` to `β`, `f'` from `α` to `β'`, and `g'` from `β'` to `γ`, if for every element `a` of type `α`, the composition `f(g(a))` equals the composition `g'(f'(a))`, then the image of the image of `s` under `g` then `f` equals the image of the image of `s` under `f'` then `g'`. In simpler terms, this theorem says that if two composite functions give the same result when applied to every element of a set, then the sets obtained by first applying one function and then the other to the entire set are also the same. More concisely: If for all `a` in a set `α`, `f(g(a)) = g'(f'(a))` for functions `f: β → γ`, `g: α → β`, `f': α → β'`, and `g': β' → γ`, then `f''(s) := {f(x) \| x ∈ s} = g''(s') := {g'(x) \| x ∈ s}` for sets `s ⊆ α` and `s' ⊆ α`.
`Set.image_id` theorem Set.image_id : ∀ {α : Type u_1} (s : Set α), id '' s = s This theorem states that for every set `s` of elements of some type `α`, the image of `s` under the identity function (`id`) is equal to `s` itself. In other words, if we apply the identity function to each element of a set, we get back the same set. This aligns with the mathematical principle that the identity function leaves all elements unchanged. More concisely: For every set `s` and all `x` in `s`, `id x ∈ s`. (In Lean, this would be expressed as `∀ s : Set α, ∀ x : α, id x ∈ s → s`)
`Set.image_symmDiff` theorem Set.image_symmDiff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s t : Set α), f '' symmDiff s t = symmDiff (f '' s) (f '' t) This theorem states that for any types `α` and `β` and any function `f` from `α` to `β`, if `f` is injective (which means that `f` maps distinct inputs to distinct outputs), then the image of the symmetric difference of two sets `s` and `t` under `f` is the same as the symmetric difference of the images of `s` and `t` under `f`. In mathematical terms, given an injective function `f: α → β` and two sets `s, t ⊆ α`, then `f` applied to the symmetric difference of `s` and `t` equals the symmetric difference of `f(s)` and `f(t)`. Here, symmetric difference is defined as `(A \ B) ⊔ (B \ A)` for sets `A` and `B`, which means the union of the set difference `A \ B` and the set difference `B \ A`. More concisely: For injective functions `f: α → β` and sets `s, t ⊆ α`, `f(s Δ t) = f(s) Δ f(t)`, where `Δ` denotes the symmetric difference.
`Subtype.range_coe` theorem Subtype.range_coe : ∀ {α : Type u_1} {s : Set α}, Set.range Subtype.val = s This theorem states that for any type `α` and for any set `s` of type `α`, the range of the subtype coercion function (i.e., `Subtype.val`) is equal to the set `s`. In other words, if you take all the elements of the subtype and retrieve their underlying elements in `α` (using `Subtype.val`), you will obtain exactly the set `s`. This underlines the correspondence between a set `s` and the subtype determined by the membership to `s` in terms of their elements. More concisely: For any subtype `s` of type `α`, the image of `s` under the subtype coercion function is equal to `s`. In mathematical notation, `Subtype.val (Subtype.mk ��igma) = ��igma`, where `��igma` is the set represented by the subtype `s`.
`Set.range_inclusion` theorem Set.range_inclusion : ∀ {α : Type u_1} {s t : Set α} (h : s ⊆ t), Set.range (Set.inclusion h) = {x \| ↑x ∈ s} This theorem, `Set.range_inclusion`, states that for any type `α` and any sets `s` and `t` of type `α`, if `s` is a subset of `t` (denoted by `s ⊆ t`), then the range of the inclusion function, which maps elements of `s` to `t`, is exactly the set `s`. In other words, the range of the inclusion function consists precisely of those elements that belong to the original subset `s`. More concisely: For any type `α` and sets `s` and `t` of type `α` with `s ⊆ t`, the range of the inclusion function from `s` to `t` equals `s`.
`Set.range_const` theorem Set.range_const : ∀ {α : Type u_1} {ι : Sort u_4} [inst : Nonempty ι] {c : α}, (Set.range fun x => c) = {c} The theorem `Set.range_const` states that for any type `α` and for any type or sort `ι` that is nonempty, the range of a function that maps each element of `ι` to a constant `c` in `α` is a set containing only the element `c`. In other words, when a function always returns the same value, the range of this function is a set with that single value. More concisely: For any constant function from a nonempty type or sort to a type, its range is a set containing only that constant.
`Subtype.range_coe_subtype` theorem Subtype.range_coe_subtype : ∀ {α : Type u_1} {p : α → Prop}, Set.range Subtype.val = {x \| p x} This theorem, `Subtype.range_coe_subtype`, states that for any type `α` and any proposition `p` that is a property of elements of `α`, the range of the function `Subtype.val` (which maps each subtype of `α` satisfying the property `p` to `α`) is exactly the set of elements of `α` that satisfy the property `p`. In other words, by mapping through `Subtype.val`, we recover exactly the set of elements in `α` that satisfy the property `p`. This theorem is marked as a simplification lemma, meaning that Lean's simplifier will use it to automatically simplify expressions in proofs. More concisely: The `Subtype.range_coe_subtype` theorem in Lean asserts that the range of the function `Subtype.val` from subtypes of a type `α` satisfying a property `p` is equal to the set of elements in `α` that satisfy `p`.
`Set.preimage_comp` theorem Set.preimage_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {s : Set γ}, g ∘ f ⁻¹' s = f ⁻¹' (g ⁻¹' s) The theorem `Set.preimage_comp` states that for all types `α`, `β`, and `γ`, and for every function `f` from `α` to `β`, a function `g` from `β` to `γ`, and a set `s` of type `γ`, the preimage of `s` under the composition of `g` and `f` is equal to the preimage of the preimage of `s` under `g` under `f`. In other words, taking the preimage under a composition of two functions is the same as taking the preimage under each function successively. This is often expressed in mathematical notation as $(g \circ f)^{-1}(s) = f^{-1}(g^{-1}(s))$. More concisely: For all types `α`, `β`, `γ`, functions `f : α → β` and `g : β → γ`, and sets `s : Set γ`, the preimage of `s` under the composition `g ∘ f` equals the preimage of the preimage of `s` under `g` under `f`, i.e., `(g ∘ f)⁻¹(s) = f⁻¹(g⁻¹(s))`.
`Set.preimage_range` theorem Set.preimage_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), f ⁻¹' Set.range f = Set.univ The theorem `Set.preimage_range` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, the preimage of the range of `f` under `f` itself is the universal set of `α`. In other words, for every element `x` in `α`, there exists an element `y` in the range of `f` (which is a subset of `β`) such that `f(x) = y`. This coincides with the definition of the universal set, which contains all elements of a given type. More concisely: For any function `f` from type `α` to type `β`, the preimage of the range of `f` under `f` equals the universe of `α`.
`Set.preimage_union` theorem Set.preimage_union : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set β}, f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t The theorem `Set.preimage_union` states that for all types `α` and `β`, for every function `f` from `α` to `β`, and for any two sets `s` and `t` of type `β`, the preimage of the union of `s` and `t` under the function `f` is equal to the union of the preimages of `s` and `t` under `f`. In mathematical notation, this can be written as $f^{-1}(s \cup t) = f^{-1}(s) \cup f^{-1}(t)$. This means that the set of all elements in `α` that map to elements in either `s` or `t` is the same as the set of all elements in `α` that map to elements in `s` combined with those that map to elements in `t`. More concisely: For all types `α` and `β`, given functions `f` from `α` to `β`, and sets `s` and `t` in `β`, the preimage of `s ∪ t` under `f` equals the union of `f⁻¹(s)` and `f⁻¹(t)`.
`Set.subsingleton_of_preimage` theorem Set.subsingleton_of_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → ∀ (s : Set β), (f ⁻¹' s).Subsingleton → s.Subsingleton The theorem `Set.subsingleton_of_preimage` states that for any two types `α` and `β` and any function `f` from `α` to `β`, if `f` is surjective (meaning that for every element `b` in `β`, there exists some element `a` in `α` such that `f(a) = b`), then for any set `s` of type `β`, if the preimage of `s` under `f` (that is, the set of all elements `a` in `α` such that `f(a)` is in `s`) is a subsingleton (meaning that it contains at most one element), then `s` itself is a subsingleton. In simpler terms, if a surjective function pulls back singletons to singletons, then the original set was a singleton. More concisely: If a surjective function maps a subsingleton to a subsingleton, then the original set is a singleton.
`Set.range_nonempty_iff_nonempty` theorem Set.range_nonempty_iff_nonempty : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, (Set.range f).Nonempty ↔ Nonempty ι This theorem states that for any function `f` from a type `ι` to another type `α`, the range of the function `f` is nonempty if and only if the type `ι` is nonempty. In other words, the function `f` has a nonempty range if there exists at least one input of type `ι` for `f`. The theorem captures the concept that a function's range can only be nonempty if there are inputs to map from, i.e., the input type is nonempty. More concisely: A function from a nonempty type to another type has a nonempty range.
`Set.image_preimage_eq_of_subset` theorem Set.image_preimage_eq_of_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, s ⊆ Set.range f → f '' (f ⁻¹' s) = s The theorem `Set.image_preimage_eq_of_subset` states that for any two types `α` and `β`, any function `f` from `α` to `β`, and any set `s` of type `β`, if `s` is a subset of the range of `f`, then the image of the preimage of `s` under `f` is equal to `s`. In simpler terms, if we take a set `s` and find all values in the domain `α` that map to `s` under `f` (this is the preimage of `s` under `f`), and then apply `f` to these values again, we get back the original set `s`. This process of "going backward" (finding the preimage) and then "going forward" (applying `f`) leaves us where we started, but only if every element of `s` is mapped to by `f`. More concisely: If `f` is a function from type `α` to type `β` and `s ⊆ Range(f)`, then `f''(⁻¹(s)) = s`.
`Disjoint.preimage` theorem Disjoint.preimage : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {s t : Set β}, Disjoint s t → Disjoint (f ⁻¹' s) (f ⁻¹' t) The theorem `Disjoint.preimage` states that for every two types `α` and `β`, and a function `f` from `α` to `β`, if two sets `s` and `t` of type `β` are disjoint, then the preimage of `s` and `t` under the function `f` are also disjoint. Here, "disjoint" means that the greatest lower bound (infimum or `⊓`) of any two elements, one from each set, is the smallest element in the set (`⊥`). The preimage of a set under a function is the set of all inputs that the function maps to elements in the set. More concisely: If `s` and `t` are disjoint sets in type `β`, then the preimages `f⁁⁻¹(s)` and `f⁁⁻¹(t)` are disjoint subsets of type `α`.
`Set.image_insert_eq` theorem Set.image_insert_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {s : Set α}, f '' insert a s = insert (f a) (f '' s) This theorem states that for any types `α` and `β`, any function `f` from `α` to `β`, any element `a` of type `α`, and any set `s` of type `α`, the image of the function `f` applied to the set that results from inserting element `a` into set `s` is equal to the set that results from inserting `f(a)` into the image of `f` applied to `s`. In mathematical terms, this could be written as $f(\{a\} \cup s) = \{f(a)\} \cup f(s)$. This theorem is related to the concept of image and the property of functions with sets. More concisely: For any functions $f: \alpha \rightarrow \beta$, elements $a:\alpha$, and sets $s:\alpha$, we have $f(\{a\} \cup s) = \{f(a)\} \cup f(s)$.
`Set.forall_range_iff` theorem Set.forall_range_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : α → Prop}, (∀ a ∈ Set.range f, p a) ↔ ∀ (i : ι), p (f i) := by sorry The theorem `Set.forall_range_iff` states that for any type `α`, any sort `ι`, any function `f: ι → α`, and any property `p` that holds for values of type `α`, it is equivalent to say that the property `p` holds for all elements in the range of the function `f`, and to say that the property `p` holds for all images of the function `f` when it is applied to any element of `ι`. In other words, checking a property on all elements in the range of a function is the same as checking the property on the image of the function for all possible inputs. More concisely: For any type `α`, sort `ι`, function `f: ι → α`, and property `p` on `α`, `∀ x ∈ ι, p(fx) ↔ ∀ x' ∈ range(f), p(x')`.
`Set.Nontrivial.image` theorem Set.Nontrivial.image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Nontrivial → ∀ {f : α → β}, Function.Injective f → (f '' s).Nontrivial The theorem `Set.Nontrivial.image` states that for any types `α` and `β`, any set `s` of type `α`, and any function `f` from `α` to `β`, if the set `s` is nontrivial (i.e., contains at least two distinct elements) and the function `f` is injective (i.e., it never maps different inputs to the same output), then the image of the set `s` under the function `f` is also nontrivial. This is to say that, when we use an injective function to map a nontrivial set to another set, the resulting set will also contain at least two distinct elements. More concisely: If `s` is a non-empty set and `f` is an injective function from `α` to `β` such that `s ≠ ∅`, then `f''s` (the image of `s` under `f`) also contains at least two distinct elements.
`Set.image_subset_iff` theorem Set.image_subset_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, f '' s ⊆ t ↔ s ⊆ f ⁻¹' t This theorem states that for any two types `α` and `β`, any set `s` of type `α`, any set `t` of type `β` and any function `f` from `α` to `β`, the image of set `s` under function `f` is a subset of set `t`, if and only if set `s` is a subset of the preimage of set `t` under function `f`. In other words, given a function, the operations of taking the image and preimage form a Galois connection between the powersets of the domain and codomain. More concisely: For any functions between types `α` and `β`, the image of a set under the function is a subset of another set if and only if the preimage of the second set under the function is a subset of the first.
`Set.exists_range_iff` theorem Set.exists_range_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : α → Prop}, (∃ a ∈ Set.range f, p a) ↔ ∃ i, p (f i) This theorem states that for any type `α`, sort `ι`, function `f` from `ι` to `α`, and property `p` on `α`, there exists an element `a` in the range of `f` such that `p(a)` holds if and only if there exists an element `i` such that `p(f(i))` holds. Essentially, this means that a property holds for some value in the range of a function if and only if it holds for the image of some input to the function. More concisely: For any function `f: ι -> α` and property `p` on `α`, the existence of an `a ∈ range f` with `p(a)` is equivalent to the existence of an `i ∈ ι` with `p(f(i))`.
`Set.image_empty` theorem Set.image_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), f '' ∅ = ∅ This theorem states that for any function `f` from an arbitrary type `α` to another arbitrary type `β`, the image of the empty set under `f` is also the empty set. In mathematical terms, if we have a function `f: α → β`, then `f(∅) = ∅`. This means that if we apply the function `f` to each element in the empty set, we will get an empty set as no elements exist to apply the function to. More concisely: For any function `f: α → β`, `f(∅) = ∅`, where `∅` denotes the empty set.
`Function.Semiconj.set_image` theorem Function.Semiconj.set_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β}, Function.Semiconj f ga gb → Function.Semiconj (Set.image f) (Set.image ga) (Set.image gb) This theorem states that for all functions `f` from type `α` to `β`, and functions `ga` from type `α` to itself and `gb` from type `β` to itself, if `f` semi-conjugates `ga` to `gb`, then the set image of `f` also semi-conjugates the set image of `ga` to the set image of `gb`. In other words, if for every element `x` of type `α`, applying `f` after `ga` yields the same result as applying `gb` after `f`, then this property also holds when considering the sets of elements obtained by applying these functions. More concisely: If function `f` semi-conjugates `ga` to `gb`, then the image of `f` maps the image of `ga` onto the image of `gb`.
`Function.LeftInverse.preimage_preimage` theorem Function.LeftInverse.preimage_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α}, Function.LeftInverse g f → ∀ (s : Set α), f ⁻¹' (g ⁻¹' s) = s The theorem `Function.LeftInverse.preimage_preimage` states that for all types `α` and `β`, and for all functions `f` from `α` to `β` and `g` from `β` to `α`, if `g` is a left inverse to `f` (that is, applying `g` after `f` results in the identity function), then for any set `s` of elements of type `α`, the preimage of the preimage of `s` under `f` followed by `g` is equal to `s` itself. In other words, applying `f` and then `g` to the elements of `s` doesn't change the set `s`. More concisely: If `f: α → β` has a left inverse `g: β → α`, then for any subset `S ⊆ α`, we have `f''(g''(S)) = S`.
`Set.image_preimage_subset` theorem Set.image_preimage_subset : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), f '' (f ⁻¹' s) ⊆ s := by sorry This theorem states that for any function `f` from an arbitrary type `α` to another arbitrary type `β`, and for any set `s` of elements of type `β`, the image under `f` of the preimage of `s` under `f` is a subset of `s`. In other words, if you take a set `s`, consider the set of all elements that get mapped into `s` by `f`, and then apply `f` to that set, you obtain a set that is contained within `s`. This is a fundamental property of the concept of a function's image and preimage. More concisely: For any function `f` from type `α` to type `β`, and any set `s` in type `β`, the image of `f` of the preimage of `s` is contained in `s`: `image (f : α → β) (preimage s : Set α) ⊆ s`.
`Set.image_subset` theorem Set.image_subset : ∀ {α : Type u_1} {β : Type u_2} {a b : Set α} (f : α → β), a ⊆ b → f '' a ⊆ f '' b := by sorry The theorem `Set.image_subset` states that, for any two sets `a` and `b` of any type `α`, and a function `f` from `α` to some type `β`, if `a` is a subset of `b` (written as `a ⊆ b`), then the image of `a` under the function `f` is a subset of the image of `b` under `f` (written as `f '' a ⊆ f '' b`). In other words, if all elements of a first set are also in a second set, then all elements in the image of the first set under `f` are also in the image of the second set under `f`. This property is known as the monotonicity of the image with respect to the subset relation. More concisely: If `a` is a subset of `b`, then `f(a)` is a subset of `f(b)` for any function `f` from a type `α` to another type `β`.
`Set.preimage_mono` theorem Set.preimage_mono : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set β}, s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t := by sorry The theorem `Set.preimage_mono` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, if a set `s` of type `β` is a subset of another set `t` of the same type, then the preimage of `s` under `f` is a subset of the preimage of `t` under `f`. Here, the preimage of a set under a function is the set of all elements in the domain that get mapped to the elements in the given set by the function. More concisely: If `s subseteq t` are subsets of type `β`, then `f⁁⁃1(s) subseteq f⁁⁃1(t)` for any function `f : α -> β` from type `α` to type `β`. (Here, `f⁁⁃1(X)` denotes the preimage of set `X` under function `f`.)
`Function.Surjective.image_preimage` theorem Function.Surjective.image_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → ∀ (s : Set β), f '' (f ⁻¹' s) = s This theorem states that for every types `α` and `β`, and for every function `f` from `α` to `β`, if the function `f` is surjective, then for every set `s` of type `β`, the image under `f` of the preimage under `f` of `s` is equal to `s`. In mathematical terms, it states that for a surjective function `f: α → β`, for all subsets `s` of `β`, `f(f⁻¹(s)) = s`. This effectively captures the property of surjective functions where every element in the codomain `β` is the image of at least one element from the domain `α`. More concisely: For every surjective function `f: α → β`, the image of `f` of the preimage of any subset `s` of `β` equals `s`.
`Set.image_preimage_eq_iff` theorem Set.image_preimage_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f '' (f ⁻¹' s) = s ↔ s ⊆ Set.range f The theorem `Set.image_preimage_eq_iff` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any set `s` of type `β`, the image of the preimage of `s` under `f` is equal to `s` if and only if `s` is a subset of the range of `f`. In other words, for every element in `s`, there exists an element in the domain of `f`, such that the function `f` maps that element to `s`. The terms `f '' (f ⁻¹' s)` and `s ⊆ Set.range f` can be translated into mathematical language as $f(f^{-1}(s)) = s$ and $s \subseteq Range(f)$ respectively. More concisely: For any function $f: \alpha \rightarrow \beta$ and set $s \subseteq \beta$, $f(f^{-1}(s)) = s$ if and only if $s \subseteq \text{Range}(f)$.
`Set.range_const_subset` theorem Set.range_const_subset : ∀ {α : Type u_1} {ι : Sort u_4} {c : α}, (Set.range fun x => c) ⊆ {c} This theorem states that for any type `α` and any sort `ι`, and for any constant `c` of type `α`, the range of the constant function (that assigns `c` to every element of `ι`) is a subset of the set containing only the constant `c`. In other words, all outputs of this constant function are indeed `c`, so the set of all these outputs (the range) is either empty (if `ι` is empty) or includes only `c`. More concisely: For any type `α`, sort `ι`, and constant `c` of type `α`, the range of the constant function from `ι` to `α` that maps all elements to `c` is a subset of the singleton set `{c}`.
`Set.Subsingleton.preimage` theorem Set.Subsingleton.preimage : ∀ {α : Type u_1} {β : Type u_2} {s : Set β}, s.Subsingleton → ∀ {f : α → β}, Function.Injective f → (f ⁻¹' s).Subsingleton The theorem `Set.Subsingleton.preimage` states that for every two types `α` and `β`, for any set `s` of type `β`, if `s` is a subsingleton (that is, it contains at most one element), and for any function `f` from `α` to `β` that is injective (meaning that different inputs produce different outputs), then the preimage of `s` under `f` (the set of all elements in `α` that `f` maps into `s`) is also a subsingleton. In other words, an injective function cannot map more than one element of `α` into a subsingleton set in `β`. More concisely: If `s` is a subsingleton set of type `β` and `f` is an injective function from type `α` to `β`, then the preimage of `s` under `f` is also a subsingleton.
`Set.range_unique` theorem Set.range_unique : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} [h : Unique ι], Set.range f = {f default} := by sorry This theorem states that the range of a function `f` originating from a 'Unique' type, denoted by `ι`, only contains the function applied to its single unique value. In other words, if `f` is a function from a type, `ι`, with only one possible value (a unique type), then the set of all possible outputs of `f` (the range of `f`) is simply the set containing just the result of applying `f` to that one possible input value. More concisely: If `f` is a function from a type with a unique value, then the range of `f` is the set containing the image of that unique value under `f`.
`Set.disjoint_image_of_injective` theorem Set.disjoint_image_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ {s t : Set α}, Disjoint s t → Disjoint (f '' s) (f '' t) This theorem states that for all types `α` and `β` and for all functions `f` from `α` to `β`, if the function `f` is injective, then for any two disjoint sets `s` and `t` of type `α`, their images under the function `f` are also disjoint. Here, two sets are considered disjoint if their intersection is the empty set, and a function is called injective if it assigns distinct outputs to distinct inputs. More concisely: If `f` is an injective function from type `α` to type `β`, then the images of any two disjoint sets `s` and `t` in `α` under `f` are also disjoint sets in `β`.
`Set.preimage_inr_image_inl` theorem Set.preimage_inr_image_inl : ∀ {α : Type u_1} {β : Type u_2} (s : Set α), Sum.inr ⁻¹' (Sum.inl '' s) = ∅ := by sorry This theorem states that for all sets `s` of some type `α`, the preimage of the image of `s` under the function `Sum.inl` through the function `Sum.inr` equals the empty set. This result arises from the fact that `Sum.inl` and `Sum.inr` are disjoint embedding functions for different types `α` and `β` into the type `Sum α β`. The image of `s` under `Sum.inl` is a set of left `Sum` elements, but the inverse image under `Sum.inr` only relates to right `Sum` elements, hence their intersection is empty. More concisely: For all sets `s` of type `α`, the preimage of the image of `s` under `Sum.inl` through `Sum.inr` is the empty set.
`Set.subsingleton_of_image` theorem Set.subsingleton_of_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), (f '' s).Subsingleton → s.Subsingleton The theorem `Set.subsingleton_of_image` states that for any types `α` and `β`, and any function `f` from `α` to `β`, if `f` is injective and the image of a set `s` (of type `α`) under `f` is a subsingleton (i.e., it contains at most one element), then the set `s` itself is a subsingleton. In other words, if an injective function maps a set to a set with at most one element, then the original set must also have at most one element. More concisely: If `f: α → β` is injective and `image f s` is a subsingleton, then `s` is a subsingleton.
`Set.mem_image_iff_bex` theorem Set.mem_image_iff_bex : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {y : β}, y ∈ f '' s ↔ ∃ x, ∃ (_ : x ∈ s), f x = y := by sorry This theorem, `Set.mem_image_iff_bex`, states that for any types `α` and `β`, a function `f` from `α` to `β`, a set `s` of elements of type `α`, and an element `y` of type `β`, `y` is in the image of the set `s` under the function `f` if and only if there exists an element `x` in the set `s` such that `f(x) = y`. In other words, an element `y` is in the image of the function `f` applied to the set `s` if and only if `y` can be written as `f(x)` for some `x` in `s`. More concisely: For any function $f : \alpha \to \beta$, set $S \subseteq \alpha$, and $\beta$-element $y$, $y \in \text{image}(f)(S)$ if and only if there exists $x \in S$ such that $f(x) = y$.
`Set.preimage_const_of_not_mem` theorem Set.preimage_const_of_not_mem : ∀ {α : Type u_1} {β : Type u_2} {b : β} {s : Set β}, b ∉ s → (fun x => b) ⁻¹' s = ∅ The theorem `Set.preimage_const_of_not_mem` states that for any types `α` and `β`, a value `b` of type `β`, and a set `s` of values of type `β`, if `b` does not belong to the set `s` (`b ∉ s`), then the preimage of the set `s` under the constant function that always returns `b` is the empty set. In other words, there are no elements of type `α` that when mapped by this constant function would land in `s`. More concisely: For any types `α` and `β`, if `b` is not an element of set `s` in `β`, then the preimage of `s` under the constant function `λ x => b` is the empty set in `α`.
`Set.Nontrivial.preimage` theorem Set.Nontrivial.preimage : ∀ {α : Type u_1} {β : Type u_2} {s : Set β}, s.Nontrivial → ∀ {f : α → β}, Function.Surjective f → (f ⁻¹' s).Nontrivial The theorem `Set.Nontrivial.preimage` states that for any two types `α` and `β`, and a set `s` of type `β`, if `s` is nontrivial (i.e., it contains at least two distinct elements), and a function `f` mapping from `α` to `β` is surjective (meaning that for every element in `β`, there is at least one element in `α` that is mapped to it by `f`), then the preimage of `s` under `f` is also nontrivial. This means that there exists at least two distinct elements in `α` that are mapped to two distinct elements of `s` by `f`. More concisely: If `s` is a non-empty set with at least two elements in `β` and `f` is a surjective function from `α` to `β`, then `f⁻¹(s)`, the preimage of `s` under `f`, contains at least two distinct elements in `α`.
`Set.range_comp` theorem Set.range_comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (g : α → β) (f : ι → α), Set.range (g ∘ f) = g '' Set.range f := by sorry The theorem `Set.range_comp` states that for any types `α`, `β`, and `ι`, and for any functions `g` from `α` to `β` and `f` from `ι` to `α`, the range of the composition of `g` and `f` is equal to the image of the range of `f` under the function `g`. In other words, if we first apply the function `f` and then apply the function `g`, it is the same as if we directly applied `g` to the set of all possible outputs of `f`. This theorem formalizes the idea of function composition in the context of set theory. More concisely: The range of the composition of functions `g : α → β` and `f : ι → α` is equal to the image of the range of `f` under `g`.
`Set.image_compl_eq` theorem Set.image_compl_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Function.Bijective f → f '' sᶜ = (f '' s)ᶜ The theorem `Set.image_compl_eq` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any set `s` of type `α`, if the function `f` is bijective (i.e., both injective and surjective), then the image under `f` of the complement of `s` (denoted by `f '' sᶜ` in Lean) is equal to the complement of the image under `f` of `s` (denoted by `(f '' s)ᶜ`). In other words, the image of the complement of a set under a bijective function equals the complement of the image of the set. More concisely: For any bijective function `f` from type `α` to type `β` and any set `s` of type `α`, the image of `s`'s complement under `f` equals the complement of `f(s)`.
`Set.subset_preimage_image` theorem Set.subset_preimage_image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), s ⊆ f ⁻¹' (f '' s) := by sorry The theorem `Set.subset_preimage_image` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, and for any set `s` of type `α`, the set `s` is a subset of the preimage under `f` of the image of `s` under `f`. In mathematical terms, this can be written as $s \subseteq f^{-1}(f(s))$. This theorem is about the relationship between a set and its image under a function: it says that every element of the original set is mapped to an element in the image, hence, the preimage of the image contains the original set. More concisely: For any function `f` and sets `s` of types `α` and `β`, `s` is a subset of the preimage of `f(s)` under `f`. In mathematical notation, `s ↪ f⁻¹(f(s))`.
`Set.monotone_image` theorem Set.monotone_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Monotone (Set.image f) The theorem `Set.monotone_image` states that for any function `f` mapping elements from a type `α` to a type `β`, the operation of taking the image of a set under `f` (`Set.image f`) is a monotone function. In other words, if we have two sets `A` and `B` such that `A` is a subset of `B` (denoted `A ⊆ B`), then the image of `A` under `f` is also a subset of the image of `B` under `f`, i.e., `f(A) ⊆ f(B)`. This property of `Set.image` is known as monotonicity. More concisely: Given a function `f` from type `α` to type `β`, the image of a subset under `f` is a subset of the image of its superset, i.e., `Set.image (f : α → β) (A ⊆ B)` implies `Set.image f A ⊆ Set.image f B`.
`Function.Injective.image_injective` theorem Function.Injective.image_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Function.Injective (Set.image f) This theorem states that for all types `α` and `β`, and for any function `f` from `α` to `β`, if `f` is injective, then the function that maps a set `s` of type `α` to the image of `s` under `f` is also injective. In mathematical terms, if `f : α → β` is an injective function, then the function `g: Set α → Set β` defined by `g(s) = f '' s` is also injective. More concisely: If `f : α → β` is an injective function, then the function `g : Set α → Set β` defined by `g(s) = {x │ ∃ (a ∈ s). f(a) = x}` is also injective. (Note: This statement assumes the set theoretic interpretation of Lean types and functions.)
`Subtype.range_val` theorem Subtype.range_val : ∀ {α : Type u_1} {s : Set α}, Set.range Subtype.val = s This theorem, named `Subtype.range_val`, states that for any type `α` and any set `s` of that type, the range of the `Subtype.val` function is equal to `s`. The `Subtype.val` function retrieves the underlying base element from a subtype. This variant is particularly useful when defining a new type as a subtype of something else, in which case the usual coercion mechanism may not work as expected. The more general version `range_coe` should be used when possible, but this version is available for those special cases. More concisely: For any type `α` and set `s` of that type, the image of `s` under the `Subtype.val` function is equal to `s`.

LeanAide GPT-4 documentation

Module: Mathlib.Data.Set.Image

Function.Surjective.preimage_subset_preimage_iff

theorem Function.Surjective.preimage_subset_preimage_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set β}, Function.Surjective f → (f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t) := by sorry

Set.exists_eq_const_of_preimage_singleton

theorem Set.exists_eq_const_of_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty β] {f : α → β}, (∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = Set.univ) → ∃ b, f = Function.const α b

Set.image_univ_of_surjective

theorem Set.image_univ_of_surjective : ∀ {β : Type u_2} {ι : Type u_6} {f : ι → β}, Function.Surjective f → f '' Set.univ = Set.univ

Set.preimage_id

theorem Set.preimage_id : ∀ {α : Type u_1} {s : Set α}, id ⁻¹' s = s

Set.image_perm

theorem Set.image_perm : ∀ {α : Type u_1} {s : Set α} {σ : Equiv.Perm α}, {a | σ a ≠ a} ⊆ s → ⇑σ '' s = s

Set.image_eq_preimage_of_inverse

theorem Set.image_eq_preimage_of_inverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α}, Function.LeftInverse g f → Function.RightInverse g f → Set.image f = Set.preimage g

Mathlib.Data.Set.Image._auxLemma.12

theorem Mathlib.Data.Set.Image._auxLemma.12 : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, (f '' s ⊆ t) = (s ⊆ f ⁻¹' t)

Set.preimage_univ

theorem Set.preimage_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f ⁻¹' Set.univ = Set.univ

Set.surjective_onto_range

theorem Set.surjective_onto_range : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, Function.Surjective (Set.rangeFactorization f)

Set.image_pair

theorem Set.image_pair : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a b : α), f '' {a, b} = {f a, f b}

Subtype.coe_image_subset

theorem Subtype.coe_image_subset : ∀ {α : Type u_1} (s : Set α) (t : Set ↑s), Subtype.val '' t ⊆ s

Set.preimage_compl

theorem Set.preimage_compl : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ

Set.Subsingleton.image

theorem Set.Subsingleton.image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Subsingleton → ∀ (f : α → β), (f '' s).Subsingleton

Set.image_eq_empty

theorem Set.image_eq_empty : ∀ {α : Type u_6} {β : Type u_7} {f : α → β} {s : Set α}, f '' s = ∅ ↔ s = ∅

Set.image_congr

theorem Set.image_congr : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Set α}, (∀ a ∈ s, f a = g a) → f '' s = g '' s

Set.range_nonempty

theorem Set.range_nonempty : ∀ {α : Type u_1} {ι : Sort u_4} [h : Nonempty ι] (f : ι → α), (Set.range f).Nonempty := by sorry

Function.Surjective.preimage_injective

theorem Function.Surjective.preimage_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → Function.Injective (Set.preimage f)

Set.image_injective

theorem Set.image_injective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective (Set.image f) ↔ Function.Injective f

Mathlib.Data.Set.Image._auxLemma.2

theorem Mathlib.Data.Set.Image._auxLemma.2 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)

Set.leftInverse_rangeSplitting

theorem Set.leftInverse_rangeSplitting : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.LeftInverse (Set.rangeFactorization f) (Set.rangeSplitting f)

Set.Nonempty.image

theorem Set.Nonempty.image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {s : Set α}, s.Nonempty → (f '' s).Nonempty

Sum.range_eq

theorem Sum.range_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ⊕ β → γ), Set.range f = Set.range (f ∘ Sum.inl) ∪ Set.range (f ∘ Sum.inr)

Set.range_quot_mk

theorem Set.range_quot_mk : ∀ {α : Type u_1} (r : α → α → Prop), Set.range (Quot.mk r) = Set.univ

Set.image_subset_range

theorem Set.image_subset_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), f '' s ⊆ Set.range f := by sorry

Set.image_inter_subset

theorem Set.image_inter_subset : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), f '' (s ∩ t) ⊆ f '' s ∩ f '' t

Set.preimage_eq_iff_eq_image

theorem Set.preimage_eq_iff_eq_image : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Bijective f → ∀ {s : Set β} {t : Set α}, f ⁻¹' s = t ↔ s = f '' t

Set.range_eq_empty_iff

theorem Set.range_eq_empty_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, Set.range f = ∅ ↔ IsEmpty ι

Set.Sum.elim_range

theorem Set.Sum.elim_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ), Set.range (Sum.elim f g) = Set.range f ∪ Set.range g

Mathlib.Data.Set.Image._auxLemma.11

theorem Mathlib.Data.Set.Image._auxLemma.11 : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, (f '' s).Nonempty = s.Nonempty

Set.range_eq_iff

theorem Set.range_eq_iff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), Set.range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b

Set.image_eq_image

theorem Set.image_eq_image : ∀ {α : Type u_1} {β : Type u_2} {s t : Set α} {f : α → β}, Function.Injective f → (f '' s = f '' t ↔ s = t) := by sorry

Set.preimage_preimage

theorem Set.preimage_preimage : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : Set γ}, f ⁻¹' (g ⁻¹' s) = (fun x => g (f x)) ⁻¹' s

Set.surjective_onto_image

theorem Set.surjective_onto_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Function.Surjective (Set.imageFactorization f s) := by sorry

Set.nontrivial_of_preimage

theorem Set.nontrivial_of_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set β), (f ⁻¹' s).Nontrivial → s.Nontrivial

Set.image_eq_range

theorem Set.image_eq_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), f '' s = Set.range fun x => f ↑x

Function.Surjective.nonempty_preimage

theorem Function.Surjective.nonempty_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → ∀ {s : Set β}, (f ⁻¹' s).Nonempty ↔ s.Nonempty

Set.preimage_const

theorem Set.preimage_const : ∀ {α : Type u_1} {β : Type u_2} (b : β) (s : Set β) [inst : Decidable (b ∈ s)], (fun x => b) ⁻¹' s = if b ∈ s then Set.univ else ∅

Set.image_nonempty

theorem Set.image_nonempty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, (f '' s).Nonempty ↔ s.Nonempty

Set.image_congr'

theorem Set.image_congr' : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Set α}, (∀ (x : α), f x = g x) → f '' s = g '' s

`Function.Surjective.preimage_subset_preimage_iff`

`Set.exists_eq_const_of_preimage_singleton`

`Set.image_univ_of_surjective`

`Set.preimage_id`

`Set.image_perm`

`Set.image_eq_preimage_of_inverse`

`Mathlib.Data.Set.Image._auxLemma.12`

`Set.preimage_univ`

`Set.surjective_onto_range`

`Set.image_pair`

`Subtype.coe_image_subset`

`Set.preimage_compl`

`Set.Subsingleton.image`

`Set.image_eq_empty`

`Set.image_congr`

`Set.range_nonempty`

`Function.Surjective.preimage_injective`

`Set.image_injective`

`Mathlib.Data.Set.Image._auxLemma.2`

`Set.leftInverse_rangeSplitting`

`Set.Nonempty.image`

`Sum.range_eq`

`Set.range_quot_mk`

`Set.image_subset_range`

`Set.image_inter_subset`

`Set.preimage_eq_iff_eq_image`

`Set.range_eq_empty_iff`

`Set.Sum.elim_range`

`Mathlib.Data.Set.Image._auxLemma.11`

`Set.range_eq_iff`

`Set.image_eq_image`

`Set.preimage_preimage`

`Set.surjective_onto_image`

`Set.nontrivial_of_preimage`

`Set.image_eq_range`

`Function.Surjective.nonempty_preimage`

`Set.preimage_const`

`Set.image_nonempty`

`Set.image_congr'`

`Set.image_union`

`Set.preimage_eq_preimage`

`Set.image_univ`

`Mathlib.Data.Set.Image._auxLemma.23`

`Function.Injective.preimage_image`

`Set.range_eq_empty`

`Set.image_singleton`

`Set.range_subset_iff`

`Set.image_preimage_inter`

`Set.isCompl_range_some_none`

`Set.image_inter_preimage`

`Set.isCompl_range_inl_range_inr`

`Function.Injective.mem_set_image`

`Set.nonempty_image_iff`

`Set.Nonempty.of_image`

`Set.powerset_insert`

`Set.preimage_inter`

`Set.image_subset_image_iff`

`Set.image_inter`

`Function.Injective.preimage_surjective`

`Set.image_preimage_eq`

`Function.Surjective.range_eq`

`Set.preimage_image_eq`

`Set.range_comp_subset_range`

`Set.nontrivial_of_image`

`Set.range_iff_surjective`

`Set.image_diff`

`Set.rightInverse_rangeSplitting`

`Set.image_comp`

`Set.subset_preimage_univ`

`Set.image_preimage_eq_range_inter`

`Set.Nonempty.image_const`

`Set.preimage_id'`

`Set.image_preimage_eq_inter_range`

`Set.preimage_empty`