Set.MapsTo.congr
theorem Set.MapsTo.congr :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β},
Set.MapsTo f₁ s t → Set.EqOn f₁ f₂ s → Set.MapsTo f₂ s t
This theorem states that for any two types `α` and `β`, any set `s` of type `α`, any set `t` of type `β`, and any two functions `f₁` and `f₂` from `α` to `β`, if `f₁` maps all elements of set `s` into set `t` (`Set.MapsTo f₁ s t`), and `f₁` and `f₂` are equal on all elements within set `s` (`Set.EqOn f₁ f₂ s`), then `f₂` also maps all elements of set `s` into set `t` (`Set.MapsTo f₂ s t`). In other words, if two functions agree over a set, and one function maps that set into another set, then the other function does the same.
More concisely: If two functions agree on a set and map that set into another set, then they have the same image under that set.
|
Set.restrictPreimage_surjective
theorem Set.restrictPreimage_surjective :
∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
Function.Surjective f → Function.Surjective (t.restrictPreimage f)
The theorem `Set.restrictPreimage_surjective` states that for any types `α` and `β`, any set `t` of type `β`, and any function `f` from `α` to `β`, if the function `f` is surjective, then the restriction of `f` onto the preimage of the set `t` is also surjective. In other words, given a surjective function `f : α → β` and a set `t` of elements in `β`, every element in `t` can be mapped from some element in the preimage of `t` under `f`, which is the subset of `α` that consists of all elements which map to elements in `t` under `f`.
More concisely: If `f : α → β` is a surjective function and `t ⊆ β` is a set, then the restriction of `f` to `f⁻¹(t) ⊆ α` is also surjective onto `t`.
|
Set.BijOn.equiv_symm
theorem Set.BijOn.equiv_symm :
∀ {α : Type u_1} {β : Type u_2} {e : α ≃ β} {s : Set α} {t : Set β}, Set.BijOn (⇑e) s t → Set.BijOn (⇑e.symm) t s
The theorem `Set.BijOn.equiv_symm` asserts that for any two types `α` and `β`, and any sets `s` of type `α` and `t` of type `β`, if there exists a bijective function `e` from `s` to `t` (represented as `Set.BijOn (⇑e) s t`), then the inverse function of `e` (represented as `⇑e.symm`) is also a bijective function, but from `t` to `s` (`Set.BijOn (⇑e.symm) t s`). In other words, if a function is bijective going one way between two sets, its inverse is also bijective going the other way.
More concisely: If `e: α → β` is a bijective function, then `e.symm: β → α` is also bijective.
|
Set.InvOn.bijOn
theorem Set.InvOn.bijOn :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
Set.InvOn f' f s t → Set.MapsTo f s t → Set.MapsTo f' t s → Set.BijOn f s t
This theorem states that if we have two functions, `f` and `f'`, which are inverses to each other on sets `s` and `t` respectively, and if `f` maps all elements of `s` into `t` and `f'` maps all elements of `t` into `s`, then `f` is a bijection from `s` to `t`. In other words, `f` is one-to-one (injective) and onto (surjective) between `s` and `t`. Note that the conditions that `f` maps `s` to `t` and `f'` maps `t` to `s` can be inferred from the respective surjectivity conditions using the properties of left and right inverses.
More concisely: If functions `f` and `f'` are mutual inverses with `f` mapping set `s` onto `t` and `f'` mapping `t` onto `s`, then `f` is a bijection from `s` to `t`.
|
Set.EqOn.symm
theorem Set.EqOn.symm :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β}, Set.EqOn f₁ f₂ s → Set.EqOn f₂ f₁ s
This theorem states that for any types `α` and `β`, any set `s` of elements of type `α`, and any two functions `f₁` and `f₂` from `α` to `β`, if `f₁` and `f₂` are equal on `s` (meaning for all elements `x` in `s`, `f₁(x)` is equal to `f₂(x)`), then `f₂` and `f₁` are also equal on `s`. In other words, the property of two functions being equal on a set is symmetric.
More concisely: If functions `f₁` and `f₂` from type `α` to type `β` are equal on a set `s` of elements from `α`, then they are equal.
|
Set.bijOn_comm
theorem Set.bijOn_comm :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {g : β → α},
Set.InvOn f g t s → (Set.BijOn f s t ↔ Set.BijOn g t s)
The theorem `Set.bijOn_comm` states that for any two types `α` and `β`, any two sets `s` of type `α` and `t` of type `β`, and any two functions `f : α → β` and `g : β → α`, if `f` is an inverse to `g` when `g` is viewed as a map from `t` to `s`, then `f` is bijective from `s` to `t` if and only if `g` is bijective from `t` to `s`. In mathematical terms, if `f` and `g` are inverses on the sets `s` and `t` respectively, then `f` is a bijection between `s` and `t` if and only if `g` is a bijection between `t` and `s`.
More concisely: For types `α` and `β`, sets `s ♂α` and `t ♂β`, and functions `f : α → β` and `g : β → α` such that `f ∘ g = idβ` and `g ∘ f = idα`, `f` is a bijection between `s` and `t` if and only if `g` is a bijection between `t` and `s`.
|
Set.range_restrictPreimage
theorem Set.range_restrictPreimage :
∀ {α : Type u_1} {β : Type u_2} (t : Set β) (f : α → β),
Set.range (t.restrictPreimage f) = Subtype.val ⁻¹' Set.range f
This theorem states that for any types `α` and `β`, for any set `t` of type `β`, and for any function `f` from `α` to `β`, the range of the restriction of `f` onto the preimage of `t` is equal to the preimage under the `val` function (that retrieves the underlying element from a subtype) of the range of `f`. In simpler terms, this theorem is about the connection between the range of a function restricted to a subset of its domain (in particular, the preimage of another set) and the range of the original function.
More concisely: For any functions \(f : \alpha \to \beta\), sets \(t \subseteq \beta\), and preimage \(s = \exists x : \beta. x \in t \land f(x) \in \operatorname{range}(f)\), \(\operatorname{range}(f|_s) = \operatorname{image}(\operatorname{val}|_{\operatorname{range}(f)}) \cap t\).
|
Function.Injective.restrictPreimage
theorem Function.Injective.restrictPreimage :
∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
Function.Injective f → Function.Injective (t.restrictPreimage f)
The theorem `Function.Injective.restrictPreimage` states that for any two types `α` and `β`, a set `t` of type `β`, and an injective function `f` from `α` to `β`, the restriction of the preimage of `f` to the set `t` is also an injective function. In layman terms, if a function doesn't map any two different elements of the input type to the same element of the output type (`α` to `β`), then this property preserves even when we limit the preimage of the function to a specific set (`t`).
More concisely: If `f : α → β` is an injective function and `t ⊆ β`, then `f⁻¹(t) : α → ℛβ(f)` is also an injective function, where `ℛβ(f)` is the range of `f` on `β`.
|
Set.MapsTo.union_union
theorem Set.MapsTo.union_union :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
Set.MapsTo f s₁ t₁ → Set.MapsTo f s₂ t₂ → Set.MapsTo f (s₁ ∪ s₂) (t₁ ∪ t₂)
The theorem `Set.MapsTo.union_union` states that for any two sets `s₁` and `s₂` of type `α` and any two sets `t₁` and `t₂` of type `β`, given a function `f` from `α` to `β`, if `f` maps every element of `s₁` to an element of `t₁` and every element of `s₂` to an element of `t₂`, then `f` also maps every element of the union of `s₁` and `s₂` to an element in the union of `t₁` and `t₂`. In other words, it proves that mapping under a function preserves the union operation.
More concisely: If functions `f` map every element of sets `s₁` and `s₂` to elements in `t₁` and `t₂`, respectively, then `f` maps every element of `s₁ ∪ s₂` to an element in `t₁ ∪ t₂`.
|
Set.MapsTo.mono_left
theorem Set.MapsTo.mono_left :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} {f : α → β},
Set.MapsTo f s₁ t → s₂ ⊆ s₁ → Set.MapsTo f s₂ t
The theorem `Set.MapsTo.mono_left` states that for any types α and β, any two sets `s₁` and `s₂` of α, a set `t` of β, and a function `f` from α to β, if `f` maps every element in `s₁` to `t` (denoted as `Set.MapsTo f s₁ t`) and `s₂` is a subset of `s₁` (denoted as `s₂ ⊆ s₁`), then `f` also maps every element in `s₂` to `t` (denoted as `Set.MapsTo f s₂ t`). In essence, it says if a function maps a larger set to another set, then it also maps any subset of that larger set to the same target set.
More concisely: If a function maps every element of a set to another set, and the smaller set is a subset of the larger set, then the function maps every element of the smaller set to the same image in the larger set.
|
Set.MapsTo.mono_right
theorem Set.MapsTo.mono_right :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : α → β},
Set.MapsTo f s t₁ → t₁ ⊆ t₂ → Set.MapsTo f s t₂
The theorem `Set.MapsTo.mono_right` states that for all types `α` and `β`, for all sets `s` of type `α`, and for two sets `t₁` and `t₂` of type `β`, if a function `f` maps elements of set `s` into set `t₁` (denoted as `Set.MapsTo f s t₁`) and all the elements of set `t₁` are also in set `t₂` (denoted as `t₁ ⊆ t₂`), then it follows that the function `f` maps elements of set `s` into set `t₂`. This theorem demonstrates the monotonicity of the mapping with respect to the right-hand (target) set: if the target set expands, the mapping still holds.
More concisely: If a function maps a set into a subset of another set, then it also maps the set into the larger set.
|
Set.piecewise_preimage
theorem Set.piecewise_preimage :
∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] (f g : α → β) (t : Set β),
s.piecewise f g ⁻¹' t = s.ite (f ⁻¹' t) (g ⁻¹' t)
The theorem `Set.piecewise_preimage` states that for any sets `s` of type `α` and `t` of type `β`, and any functions `f` and `g` from `α` to `β`, the preimage of `t` under the piecewise function defined by `s`, `f`, and `g` is the "if-then-else" combination of the preimages of `t` under `f` and `g`, respectively. Specifically, this means that each element in the domain that is mapped into `t` by the piecewise function comes either from `s` and is mapped there by `f`, or from the complement of `s` and is mapped there by `g`.
More concisely: For sets $S \subseteq \alpha$ and $T \subseteq \beta$, and functions $f, g : \alpha \to \beta$, the preimage of $T$ under the piecewise function $x \mapsto if h x \in S then f x else g x$ is $f^{-1}(T) \cup g^{-1}(T)$, where $h : \alpha \to \texttt{Prop}$ is any decidable relation such that $x \in S$ if and only if $h x$.
|
Set.bijective_iff_bijOn_univ
theorem Set.bijective_iff_bijOn_univ :
∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Bijective f ↔ Set.BijOn f Set.univ Set.univ
This theorem states that for any two types `α` and `β` and a function `f` from `α` to `β`, the function `f` is bijective if and only if `f` is bijective on the universal sets of `α` and `β`. In other words, a function `f` is both injective (each element of `α` maps to a unique element of `β`) and surjective (every element of `β` is the image of some element of `α`) if and only if the same properties hold when considering all elements of the types `α` and `β`.
More concisely: A function between types is bijective if and only if it is both injective and surjective on their universal sets.
|
Set.InjOn.injective
theorem Set.InjOn.injective :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → Function.Injective (s.restrict f) := by
sorry
This theorem, referred to as an alias of the forward direction of `Set.injOn_iff_injective`, states that for any types `α` and `β`, any set `s` of type `α`, and any function `f` from `α` to `β`, if `f` is injective on the set `s` (meaning that for any two elements in `s`, if `f` maps them to the same value then they must be the same element), then the restriction of `f` to `s` is also injective. This means that, when we restrict `f` to the subset `s` of its domain and then consider it as a function from `s` to `β`, it still has the property that equal outputs mean equal inputs.
More concisely: If a function restricted to a subset is injective on that subset whenever it is injective on the entire domain, then function injectivity is preserved under subset restriction.
|
Function.LeftInverse.leftInvOn
theorem Function.LeftInverse.leftInvOn :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α},
Function.LeftInverse f g → ∀ (s : Set β), Set.LeftInvOn f g s
The theorem `Function.LeftInverse.leftInvOn` states that for any types `α` and `β`, and functions `f : α → β` and `g : β → α`, if `f` is a left inverse of `g` (i.e., `f ∘ g = id`), then `f` is also a left inverse of `g` on any set `s` of type `β`. In other words, for every element `x` in set `s`, we have `f(g(x)) = x`. This theorem shows how the global property of being a left inverse carries over to any subset of the domain.
More concisely: If `f : α → β` and `g : β → α` are such that `f ∘ g = id_β`, then `f` restricts to a left inverse of `g` on any subset `s` of `β`, i.e., `∀ x ∈ s, f(g(x)) = x`.
|
Set.LeftInvOn.image_inter'
theorem Set.LeftInvOn.image_inter' :
∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : α → β} {f' : β → α},
Set.LeftInvOn f' f s → f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s
The theorem `Set.LeftInvOn.image_inter'` states that for any types `α` and `β`, any sets `s` and `s₁` of type `α`, and any functions `f: α → β` and `f': β → α`, if `f'` is a left inverse to `f` on `s` (meaning `f' (f x) = x` for all `x` in `s`), then the image of the intersection of `s₁` and `s` under `f` is equal to the intersection of the preimage of `s₁` under `f'` and the image of `s` under `f`. In mathematical terms, if `f'∘f(x) = x` for all `x` in `s`, then `f(s₁ ∩ s) = f'^(-1)(s₁) ∩ f(s)`.
More concisely: If `f: α → β` has a left inverse `f'` on set `s ⊆ α`, then `f(s₁ ∩ s) = f'⁻¹(s₁) ∩ f(s)` for any sets `s₁ ⊆ α`.
|
Set.injective_codRestrict
theorem Set.injective_codRestrict :
∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s),
Function.Injective (Set.codRestrict f s h) ↔ Function.Injective f
The theorem `Set.injective_codRestrict` states that for any type `α` and `ι`, any function `f` from `ι` to `α`, and any set `s` of `α`, given that for all `x` in `ι`, `f(x)` is in `s`, the function `f` restricted to the codomain `s` is injective if and only if the original function `f` is injective. In other words, restricting the codomain of an injective function to a subset does not change its injective property.
More concisely: If `f: ι → α` is an injective function and `s ⊆ α` is a set such that `∀ x ∈ ι, f x ∈ s`, then the restriction of `f` to `s`, denoted `f | s`, is also an injective function.
|
Set.SurjOn.exists_bijOn_subset
theorem Set.SurjOn.exists_bijOn_subset :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
Set.SurjOn f s t → ∃ s' ⊆ s, Set.BijOn f s' t
The theorem `Set.SurjOn.exists_bijOn_subset` states that for any given types `α` and `β`, a set `s` of type `α`, a set `t` of type `β`, and a function `f` from `α` to `β`, if the function `f` surjectively maps onto set `t` from set `s`, then there exists a subset `s'` of `s` such that `f` is bijective when mapping from this subset `s'` to the set `t`. In simpler terms, if every element of `t` has a pre-image in `s` under `f`, there exists a smaller or equal set `s'` in `s` where `f` is both injective and surjective, i.e., it maintains a one-to-one correspondence between `s'` and `t`.
More concisely: If `f`: `α` -> `β` surjectively maps `s` onto `t`, then there exists a subset `s'` of `s` such that `f` is a bijection from `s'` to `t`.
|
Set.MapsTo.restrict_surjective_iff
theorem Set.MapsTo.restrict_surjective_iff :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t),
Function.Surjective (Set.MapsTo.restrict f s t h) ↔ Set.SurjOn f s t
The theorem `Set.MapsTo.restrict_surjective_iff` states that for any types `α` and `β`, a set `s` of type `α`, a set `t` of type `β`, and a function `f` from `α` to `β` that maps `s` to `t`, the function `f` restricted to the domain `s` and codomain `t` is surjective if and only if `f` is surjective from `s` to `t`. In other words, for every element in the set `t`, there exists an element in the set `s` such that the function `f` maps this element of `s` to the element of `t`.
More concisely: For any functions $f: \alpha \to \beta$ and sets $s \subseteq \alpha$, $t \subseteq \beta$ such that $f(s) = t$, the restriction $f|_s: s \to t$ is surjective if and only if $f$ is surjective from $\alpha$ to $\beta$.
|
Set.mapsTo_univ
theorem Set.mapsTo_univ : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.MapsTo f s Set.univ
The theorem `Set.mapsTo_univ` asserts that for all types `α` and `β`, and for any function `f` from `α` to `β`, and for any set `s` of elements of type `α`, the function `f` maps the set `s` into the universal set of `β`. In other words, the image of any element in `s` under `f` is an element in `β`. This follows from the definition of `Set.univ`, which contains all elements of `β` and thus the image of any function into `β` must be contained in `Set.univ`.
More concisely: For any type `α`, type `β`, set `s` of `α`, and function `f` from `α` to `β`, `f` maps `s` into the universal set `Set.univ` of `β`, that is, for all `x in s`, `f x isin Set.univ`.
|
Set.injective_iff_injOn_univ
theorem Set.injective_iff_injOn_univ :
∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f ↔ Set.InjOn f Set.univ
The theorem `Set.injective_iff_injOn_univ` states that for all types `α` and `β` and a function `f` from `α` to `β`, the function `f` is injective (meaning that if `f x = f y`, then `x = y`) if and only if `f` is injective on the universal set of `α` (meaning that for all elements `x₁` and `x₂` in the set of all elements of `α`, if `f x₁ = f x₂`, then `x₁ = x₂`). This theorem thus provides a relationship between the general concept of function injectivity and the more specific concept of injectivity on a particular set, namely the universal set containing all elements of a type.
More concisely: A function between types is injective if and only if it is injective when restricted to the universal set.
|
Set.BijOn.image_eq
theorem Set.BijOn.image_eq :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → f '' s = t
This theorem states that for any two types `α` and `β`, and for any sets `s` of type `α` and `t` of type `β`, and any function `f` mapping from `α` to `β`, if the function `f` is bijective from set `s` to set `t` (i.e., `f` is injective on `s` and `f` maps `s` to `t`), then the image of set `s` under function `f` is equal to set `t`. In mathematical terms, we can say that for a bijective function `f : α → β`, `f(s) = t`.
More concisely: For any sets `s` of type `α` and `t` of type `β`, and any bijective function `f : α → β`, `f(s) = t`.
|
StrictAntiOn.injOn
theorem StrictAntiOn.injOn :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictAntiOn f s → Set.InjOn f s
The theorem `StrictAntiOn.injOn` states that for any two types `α` and `β`, where `α` has a linear order structure and `β` has a preorder structure, and given a function `f` from `α` to `β` and a set `s` of type `α`, if it is the case that the function `f` is strictly antitone on the set `s` (meaning, for all `a, b` in `s`, `a < b` implies `f(b) < f(a)`), then it must also be true that `f` is injective on `s` (that is, for any two elements `x₁, x₂` from `s`, if `f(x₁)` is equal to `f(x₂)`, then `x₁` must be equal to `x₂`). In other words, a strict antitone function on a set is also injective on that set.
More concisely: If `f` is a strictly antitone function from a linearly ordered type `α` to a preordered type `β`, then `f` is injective on any subset `s` of `α` where `f` is strictly antitone.
|
StrictMonoOn.injOn
theorem StrictMonoOn.injOn :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMonoOn f s → Set.InjOn f s
This theorem states that for all types `α` and `β`, where `α` is a linearly ordered set and `β` is a preordered set, for any function `f` from `α` to `β` and any set `s` of type `α`, if the function `f` is strictly monotone on the set `s`, then `f` is also injective on the set `s`. In other words, if a function strictly increases or decreases on a certain set, then it does not map different elements to the same value within that set.
More concisely: If `f` is a function from a linearly ordered set `α` to a preordered set `β`, and `f` is strictly monotone on a set `s` ⊆ `α`, then `f` is injective on `s`.
|
Set.restrict_dite
theorem Set.restrict_dite :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : (x : α) → Decidable (x ∈ s)] (f : (a : α) → a ∈ s → β)
(g : (a : α) → a ∉ s → β), (s.restrict fun a => if h : a ∈ s then f a h else g a h) = fun a => f ↑a ⋯
This theorem, `Set.restrict_dite`, states that for any types `α` and `β`, any set `s` of type `α`, and any two functions `f` and `g` of type `(a: α) → a ∈ s → β` and `(a: α) → a ∉ s → β` respectively, the restriction of the function `(a: α) => if h: a ∈ s then f a h else g a h` to the set `s` is equal to the function `(a: α) => f ↑a ` followed by ellipsis (⋯). Here, the function `f` is defined for elements in the set `s`, and the function `g` is defined for elements not in the set `s`. The theorem essentially explains how to restrict a piecewise-defined function to a set in terms of its defining functions.
More concisely: For any sets `α` and `β`, and functions `f` and `g` defined on `α`, the restriction of the piecewise function `a mapsto if a ∈ s then f a else g a` to the set `s` is equal to the function `a mapsto f (interior_of s a)`.
|
Set.SurjOn.mapsTo_invFunOn
theorem Set.SurjOn.mapsTo_invFunOn :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [inst : Nonempty α],
Set.SurjOn f s t → Set.MapsTo (Function.invFunOn f s) t s
This theorem states that for all types `α` and `β`, for any sets `s` of type `α` and `t` of type `β`, and for any function `f` from `α` to `β`, given that `α` is nonempty, if `f` is a surjective function from `s` to `t`, then the inverse function of `f` on the domain `s` maps `t` into `s`. In other words, if for every element in `t`, there is an element in `s` such that the function `f` applied on this element of `s` gives the element of `t` (which is the definition of surjectivity of `f` from `s` to `t`), then every element of `t`, when the inverse function is applied on it, will fall into set `s`.
More concisely: If `α` is nonempty and `f` is a surjective function from a set `s` of type `α` to a set `t` of type `β`, then the inverse function of `f` maps `t` into `s`.
|
Set.SurjOn.cancel_right
theorem Set.SurjOn.cancel_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g₁ g₂ : β → γ},
Set.SurjOn f s t → Set.MapsTo f s t → (Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s ↔ Set.EqOn g₁ g₂ t)
This theorem, `Set.SurjOn.cancel_right`, states that for any three types `α`, `β`, and `γ`, any sets `s` of `α` and `t` of `β`, and any functions `f : α → β` and `g₁, g₂ : β → γ`, if `f` is surjective from `s` to `t`, and the image of `s` under `f` is contained in `t`, then the functions `g₁` and `g₂` are equal on the image of `s` under `f` if and only if they are equal on `t`. In simpler terms, if `f` maps `s` onto `t` and two functions `g₁` and `g₂` agree on the image of `s` under `f`, then `g₁` and `g₂` also agree on `t`.
More concisely: If `f : α → β` is surjective from `s ⊆ α` to `t ⊆ β` and `s = f⁻¹[t]`, then `g₁ = g₂` on `t` implies `g₁ = g₂` on `s`.
|
Set.injOn_id
theorem Set.injOn_id : ∀ {α : Type u_1} (s : Set α), Set.InjOn id s
This theorem states that for any set `s` of some type `α`, the identity function `id` is injective on `s`. In other words, if `x₁` and `x₂` are elements of `s` such that `id(x₁)` equals `id(x₂)`, then `x₁` must be equal to `x₂`. This injectivity property ensures that the identity function does not map distinct elements of `s` to the same element.
More concisely: The identity function on a set `s` is a injection: if `x₁` and `x₂` are in `s` and `id(x₁) = id(x₂)`, then `x₁ = x₂`.
|
Set.piecewise_le
theorem Set.piecewise_le :
∀ {α : Type u_1} {δ : α → Type u_7} [inst : (i : α) → Preorder (δ i)] {s : Set α}
[inst_1 : (j : α) → Decidable (j ∈ s)] {f₁ f₂ g : (i : α) → δ i},
(∀ i ∈ s, f₁ i ≤ g i) → (∀ i ∉ s, f₂ i ≤ g i) → s.piecewise f₁ f₂ ≤ g
The theorem `Set.piecewise_le` states that for any type `α` and a function `δ` that maps `α` to a type with a `Preorder` structure (i.e., a type that has a partial order satisfying transitivity and reflexivity), given a set `s` of type `α` and three functions `f₁`, `f₂`, and `g` of type α to δ, if `f₁` is less than or equal to `g` for all elements of `s`, and `f₂` is less than or equal to `g` for all elements not in `s`, then the piecewise function defined by `s`, `f₁`, `f₂` (which is equal to `f₁` on `s` and to `f₂` on the complement of `s`) is less than or equal to `g`. This theorem essentially states that if a function is less than or equal to another function on a set and its complement, then the piecewise function defined by these two functions is also less than or equal to the latter function.
More concisely: Given a preorder type `δ`, a set `s` of an arbitrary type `α`, and functions `f₁`, `f₂`, and `g` from `α` to `δ` such that `f₁ ≤ g` on `s` and `f₂ ≤ g` on the complement of `s`, then the piecewise function `(λx, if x ∈ s then f₁ x else f₂ x)` is less than or equal to `g`.
|
Set.piecewise_eq_of_mem
theorem Set.piecewise_eq_of_mem :
∀ {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)] {i : α},
i ∈ s → s.piecewise f g i = f i
The theorem `Set.piecewise_eq_of_mem` states that for any type `α`, any dependent type `δ` that depends on `α`, any set `s` of type `α`, any two functions `f` and `g` from `α` to `δ`, and any instance of a decidable predicate that determines whether an element of `α` is in the set `s`, if an element `i` from `α` is in the set `s`, then the piecewise function defined by `s`, `f`, and `g` at `i` is equal to the function `f` at `i`. In other words, when an element is a member of the specified set, the piecewise function behaves exactly as the function `f`.
More concisely: If `i` is an element of set `s` in type `α`, then the piecewise function `(λ x, if h : x ∈ s then f x else g x)` equals function `f` at `i`.
|
Mathlib.Data.Set.Function._auxLemma.25
theorem Mathlib.Data.Set.Function._auxLemma.25 :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {b : β}, Set.BijOn f {a} {b} = (f a = b)
The theorem states that for any types `α` and `β`, any function `f` from `α` to `β`, and any elements `a` from `α` and `b` from `β`, the function `f` is bijective from the set containing only `a` to the set containing only `b` if and only if `f(a)` equals `b`. In other words, a function `f` provides a bijective mapping from a singleton set `{a}` to another singleton set `{b}` precisely when the application of `f` to `a` yields `b`.
More concisely: A function from type `α` to type `β` is a bijection from the singleton set `{a : α}` to the singleton set `{b : β}` if and only if `f a = b`.
|
Set.BijOn.mk
theorem Set.BijOn.mk :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
Set.MapsTo f s t → Set.InjOn f s → Set.SurjOn f s t → Set.BijOn f s t
This theorem establishes the conditions under which a function `f` is bijective from one set `s` to another set `t`. Specifically, it states that for any types `α` and `β`, and for any sets `s` of type `α` and `t` of type `β`, if the function `f` maps `s` into `t`, the function `f` is injective on `s`, and `f` is surjective from `s` to `t`, then `f` is bijective from `s` to `t`. In other words, every element of `s` is mapped to a unique element in `t` by `f`, and every element of `t` is the image of some element in `s` under `f`.
More concisely: If a function `f` maps a set `s` to another set `t` and is both injective on `s` and surjective from `s` to `t`, then `f` is a bijection from `s` to `t`.
|
Set.eqOn_union
theorem Set.eqOn_union :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f₁ f₂ : α → β},
Set.EqOn f₁ f₂ (s₁ ∪ s₂) ↔ Set.EqOn f₁ f₂ s₁ ∧ Set.EqOn f₁ f₂ s₂
The theorem `Set.eqOn_union` states that for any two types `α` and `β`, any two sets `s₁` and `s₂` of type `α`, and any two functions `f₁` and `f₂` from `α` to `β`, the functions `f₁` and `f₂` are equal on the union of `s₁` and `s₂` if and only if `f₁` and `f₂` are equal on `s₁` and `f₁` and `f₂` are equal on `s₂`. In other words, two functions are equal over the union of two sets if they are equal over each of the sets individually.
More concisely: For sets `s₁` and `s₂` of type `α` and functions `f₁` and `f₂` from `α` to `β`, `f₁ = f₂` on `s₁ ∪ s₂` if and only if `f₁ = f₂` on `s₁` and `f₁ = f₂` on `s₂`.
|
Set.surjective_mapsTo_image_restrict
theorem Set.surjective_mapsTo_image_restrict :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Function.Surjective (Set.MapsTo.restrict f s (f '' s) ⋯)
The theorem `Set.surjective_mapsTo_image_restrict` states that for any given function `f` from type `α` to type `β` and a set `s` of type `α`, the function obtained by restricting the domain of `f` to `s` and the codomain to the image of `s` under `f` (i.e., `Set.MapsTo.restrict f s (f '' s)`) is surjective. In other words, for any element in the image of `s` under `f`, there exists an element in `s` such that applying the restricted function to this element yields the given element in the image.
More concisely: For any function `f` from type `α` to type `β` and set `s` of type `α`, the restriction of `f` to `s` and its image under `f` is a surjective function.
|
Set.InjOn.mono
theorem Set.InjOn.mono :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f : α → β}, s₁ ⊆ s₂ → Set.InjOn f s₂ → Set.InjOn f s₁
The theorem `Set.InjOn.mono` states that for all types `α` and `β`, and for all sets `s₁` and `s₂` of type `α` and any function `f` from type `α` to `β`, if `s₁` is a subset of `s₂` and `f` is injective on `s₂`, then `f` is also injective on `s₁`. In other words, if we have a function that does not map two different elements to the same element in the larger set, it will also have this property in any subset of that larger set.
More concisely: If `s₁ ⊆ s₂` and `f : α → β` is injective on `s₂`, then `f` is injective on `s₁`.
|
Function.Injective.codRestrict
theorem Function.Injective.codRestrict :
∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s),
Function.Injective f → Function.Injective (Set.codRestrict f s h)
This theorem states that if a function `f : ι → α` is injective, meaning all its inputs map to unique outputs, and if for all elements `x` in the domain `ι`, `f(x)` is an element of a set `s` in `α`, then the function `f` restricted to the codomain `s`, denoted by `Set.codRestrict f s h`, is also injective. Essentially, the injectiveness of a function `f` is preserved when its codomain is restricted to a set `s`.
More concisely: If `f : ι -> α` is an injective function with image in a set `s` in `α`, then `Set.codRestrict f s` is an injective function.
|
Equiv.bijOn
theorem Equiv.bijOn :
∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α} {t : Set β},
(∀ (a : α), e a ∈ t ↔ a ∈ s) → Set.BijOn (⇑e) s t
This theorem, named `Equiv.bijOn`, states that for any two types `α` and `β` and a function `e` which is a bijection between `α` and `β`, if for every element `a` of type `α` the property holds that `a` is in set `s` if and only if `e(a)` is in set `t`, then the function `e` is a bijection between set `s` of type `α` and set `t` of type `β`. Here, a bijection means that `e` is injective (no two different elements in `s` map to the same element in `t`) and surjective (every element in `t` is the image of some element in `s`) on the given sets.
More concisely: If `e: α → β` is a bijection between types `α` and `β`, and for all `a: α`, `a ∈ s` if and only if `e(a) ∈ t`, then `e` is a bijection between sets `s ⊆ α` and `t ⊆ β`.
|
Function.update_comp_eq_of_not_mem_range
theorem Function.update_comp_eq_of_not_mem_range :
∀ {α : Sort u_6} {β : Type u_7} {γ : Sort u_8} [inst : DecidableEq β] (g : β → γ) {f : α → β} {i : β} (a : γ),
i ∉ Set.range f → Function.update g i a ∘ f = g ∘ f
The theorem `Function.update_comp_eq_of_not_mem_range` states that for any types or sorts `α`, `β`, and `γ` where `β` has decidable equality, for any functions `g : β → γ` and `f : α → β`, for any element `i : β` and any element `a : γ`, if `i` is not in the range of `f` then the composition of the updated `g` (where `g` is updated at `i` to `a`) with `f` is the same as the composition of `g` with `f`. In other words, updating the function `g` at a point not mapped to by `f` does not change the composition `g ∘ f`.
More concisely: If `f : α → β` and `g : β → γ` are functions with decidable equality on `β`, and `i ∈ β` is not in the image of `f`, then `(Function.update g i a) ∘ f = g ∘ f`, where `a ∈ γ`.
|
Set.surjOn_image
theorem Set.surjOn_image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.SurjOn f s (f '' s)
The theorem `Set.surjOn_image` states that for any types `α` and `β`, and any function `f` from `α` to `β`, and any set `s` of type `α`, the function `f` is surjective from the set `s` to its image under the function `f`. In other words, every element in the image of `s` under `f` (denoted as `f '' s`) comes from an element in `s` by applying the function `f`. This is a property of surjectivity restricted to a specific domain (`s`) and codomain (`f '' s`).
More concisely: For any function `f` from type `α` to type `β` and any set `s` of type `α`, the image `f'' s` is a subset of `{x : β | ∃ (a : α), f a = x}` (the image of `s` under `f` is equal to the set of all images of elements in `s`). In other words, `f` is surjective from `s` to its image.
|
Set.piecewise_op₂
theorem Set.piecewise_op₂ :
∀ {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
{δ' : α → Sort u_7} {δ'' : α → Sort u_8} (f' g' : (i : α) → δ' i) (h : (i : α) → δ i → δ' i → δ'' i),
(s.piecewise (fun x => h x (f x) (f' x)) fun x => h x (g x) (g' x)) = fun x =>
h x (s.piecewise f g x) (s.piecewise f' g' x)
The theorem `Set.piecewise_op₂` states that for any type `α`, function type `δ`, set `s` of type `α`, functions `f` and `g` from `α` to `δ`, a decidable instance for membership in `s`, and additional function types `δ'` and `δ''`, as well as functions `f'` and `g'` from `α` to `δ'`, and a function `h` from `α` and `δ` and `δ'` to `δ''`. The function `h` applied in a piecewise manner (i.e., different on the set `s` and its complement) using `f` and `f'` or `g` and `g'` is the same as the function `h` applied to the piecewise application of `f` and `g`, and separately to the piecewise application of `f'` and `g'`.
In other words, applying a function in a piecewise manner to the outputs of two other functions applied in a piecewise manner is the same as applying the function to the piecewise applications of the two other functions.
More concisely: Given sets `α`, types `δ`, `δ'`, `δ''`, functions `f, g : α -> δ`, `f' : α -> δ'`, `g' : α -> δ'`, and functions `h : α x δ x δ' -> δ''` decidable `s : Set α`, the piecewise application of `h` using `f` and `f'` on `s` and its complement is equal to the separate piecewise applications of `h` on the piecewise applications of `f` and `f'`.
|
Set.mapsTo_id
theorem Set.mapsTo_id : ∀ {α : Type u_1} (s : Set α), Set.MapsTo id s s
This theorem states that for any set `s` of a certain type `α`, the identity function (`id`) maps `s` to itself. In other words, if you take an element `x` from the set `s`, applying the identity function to `x` will always result in an element that is within `s`. This can also be described as: the image of the set `s` under the identity function is contained within `s` itself.
More concisely: For any set `s` and all elements `x` in `s`, `id x ∈ s`. (Here, `id` denotes the identity function.)
|
Set.codRestrict_restrict
theorem Set.codRestrict_restrict :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : ∀ (x : ↑s), f ↑x ∈ t),
Set.codRestrict (s.restrict f) t h = Set.MapsTo.restrict f s t ⋯
The theorem `Set.codRestrict_restrict` states that for any sets `s` and `t` of arbitrary types `α` and `β` respectively, and any function `f : α → β`, if for every element `x` in `s`, `f` maps `x` into `t`, then restricting the domain of `f` to `s` and then the codomain to `t` is equivalent to applying `MapsTo.restrict` on `f` with respect to `s` and `t`. In other words, applying these two restrictions in sequence is the same as directly restricting the function `f` both in its domain and codomain using `MapsTo.restrict`.
More concisely: For any sets `s` and `t` and function `f : α → β`, if `f(x) ∈ t` for all `x ∈ s`, then `Restrict (Restrict f s) t = MapsTo.restrict f s t`.
|
Set.BijOn.of_equiv_symm
theorem Set.BijOn.of_equiv_symm :
∀ {α : Type u_1} {β : Type u_2} {e : α ≃ β} {s : Set α} {t : Set β}, Set.BijOn (⇑e.symm) t s → Set.BijOn (⇑e) s t
This theorem states that for any two types `α` and `β`, and a bijective function `e` from `α` to `β`, if the inverse of `e` is bijective from a set `t` of type `β` to a set `s` of type `α`, then `e` is bijective from `s` to `t`. In other words, if we have a bijection from `t` to `s` using the inverse of `e`, we can also establish a bijection from `s` to `t` using `e` itself. Here, a function is considered bijective on particular sets if it is both injective (no two different elements in the domain map to the same element in the codomain) and surjective (every element in the codomain is the image of some element in the domain) when restricted to those sets.
More concisely: If `e: α → β` is a bijective function and `f: β → α` is its inverse, then `e` is bijective from the domain of `f` to its range.
|
Set.EqOn.image_eq_self
theorem Set.EqOn.image_eq_self : ∀ {α : Type u_1} {s : Set α} {f : α → α}, Set.EqOn f id s → f '' s = s
This theorem, `Set.EqOn.image_eq_self`, states that for any set `s` of type `α` and for any function `f` from `α` to `α`, if `f` is equal to the identity function on the set `s` (that is, for all `x` in `s`, `f(x)` equals `x`), then the image of `s` under `f` is the same as `s`. In other words, every element in `s` maps to itself under `f`, so the set of images under `f` is the same as the original set.
More concisely: If a function from a set to itself is the identity function on that set, then the image of the set under the function is equal to the set itself.
|
Set.MapsTo.mono
theorem Set.MapsTo.mono :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
Set.MapsTo f s₁ t₁ → s₂ ⊆ s₁ → t₁ ⊆ t₂ → Set.MapsTo f s₂ t₂
The theorem `Set.MapsTo.mono` states that for any two types `α` and `β`, given two sets `s₁` and `s₂` of type `α`, two sets `t₁` and `t₂` of type `β`, and a mapping function `f` from `α` to `β`, if `f` maps every element in `s₁` to `t₁` (i.e., `Set.MapsTo f s₁ t₁`), `s₂` is a subset of `s₁` (i.e., `s₂ ⊆ s₁`), and `t₁` is a subset of `t₂` (i.e., `t₁ ⊆ t₂`), then `f` also maps every element in `s₂` to `t₂` (i.e., `Set.MapsTo f s₂ t₂`). In essence, this theorem gives us certain conditions under which we can be sure that mapping a subset of a given set through a given function will result in a subset of the mapped set.
More concisely: If `f` maps every element in `s₁` to `t₁`, `s₂ ⊆ s₁`, and `t₁ ⊆ t₂`, then `f` maps every element in `s₂` to `t₂`.
|
Set.piecewise_eqOn
theorem Set.piecewise_eqOn :
∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] (f g : α → β),
Set.EqOn (s.piecewise f g) f s
The theorem `Set.piecewise_eqOn` states that for any set `s` of elements of type `α` and any two functions `f` and `g` from `α` to `β`, the function that is defined by `Set.piecewise` to be `f` on the set `s` and `g` outside of `s`, is equal to the function `f` on the set `s`. In other words, if `x` is an element of `s`, then the value of the piecewise function at `x` is the same as the value of `f` at `x`.
More concisely: For any set `s` and functions `f` and `g` from a type `α` to a type `β`, the function `Set.piecewise f g` equals `f` on the set `s`.
|
Function.Bijective.restrictPreimage
theorem Function.Bijective.restrictPreimage :
∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
Function.Bijective f → Function.Bijective (t.restrictPreimage f)
This theorem states that for any types `α` and `β`, any set `t` of type `β`, and any function `f` from `α` to `β`, if the function `f` is bijective, then the function obtained by restricting the preimage of `f` to the set `t` is also bijective. The function `t.restrictPreimage f` is a mapping that has the same domain and range as `f`, but its behavior is undefined for elements not in `t`. Thus, this theorem is about the preservation of bijectivity under the operation of restricting the preimage of a function to a set.
More concisely: If `f` is a bijective function from type `α` to type `β`, then the restriction of `f`'s preimage to any set `t` of type `β` is also a bijective function.
|
Set.InjOn.bijOn_image
theorem Set.InjOn.bijOn_image :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → Set.BijOn f s (f '' s)
This theorem, referred to as `Set.InjOn.bijOn_image`, states that for any two types `α` and `β`, a set `s` of type `α` and a function `f` mapping from `α` to `β`, if the function `f` is injective on the set `s` (meaning that for every two different elements in `s`, their images under `f` are also different), then `f` is also bijective from `s` to the image of `s` under `f` (denoted as `f '' s`). In other words, `f` not only maps distinct elements of `s` to distinct elements in its image, but also every element in the image of `s` comes from an element in `s` (surjective), thereby establishing a one-to-one correspondence between `s` and `f '' s` (bijective).
More concisely: If a function from a set to another set is injective on a subset, then it is bijective from that subset to its image.
|
Function.Injective.injOn
theorem Function.Injective.injOn :
∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), Set.InjOn f s
This theorem, referred to as an alias of `Set.injOn_of_injective`, states that for all types `α` and `β`, and for any function `f` from `α` to `β`, if `f` is injective then it is also injective on any subset `s` of `α`. In other words, if `f` is a function such that any two different elements in `α` have different images in `β`, then this property holds true not just for the elements of `α`, but also for any subset of `α`.
More concisely: If `f` is an injective function from type `α` to type `β`, then `f` is injective on any subset `s` of `α`.
|
Function.Surjective.restrictPreimage
theorem Function.Surjective.restrictPreimage :
∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
Function.Surjective f → Function.Surjective (t.restrictPreimage f)
This theorem, named `Function.Surjective.restrictPreimage`, states that for any two types `α` and `β`, a set `t` of type `β`, and a function `f` that maps from `α` to `β`, if the function `f` is surjective, then the restriction of `f` to the preimage of `t` is also surjective. In other words, if every element of `β` is associated with an element of `α` by the function `f`, then the same holds true when `f` is restricted to those elements of `α` that map into the set `t`. This restriction is performed by the `restrictPreimage` operation on the set `t`.
More concisely: If `f` is a surjective function from `α` to `β`, then the restriction of `f` to the preimage of a set `t` in `β` is also surjective onto `t`.
|
Set.MapsTo.image_subset
theorem Set.MapsTo.image_subset :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s t → f '' s ⊆ t
The theorem `Set.MapsTo.image_subset` states that for any two types `α` and `β`, and for any two sets `s` (which is a set of elements of type `α`) and `t` (which is a set of elements of type `β`), along with a function `f` from `α` to `β`, if `f` maps every element of `s` to an element of `t` (expressed as `Set.MapsTo f s t`), then the image of set `s` under function `f` (denoted by `f '' s`) is a subset of set `t`. This means every element of `f '' s` is also an element of `t`.
More concisely: If `f` maps every element of set `s` to an element in set `t`, then `f(s) ⊆ t`. (The image of set `s` under function `f` is a subset of set `t`. )
|
Set.EqOn.mono
theorem Set.EqOn.mono :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f₁ f₂ : α → β}, s₁ ⊆ s₂ → Set.EqOn f₁ f₂ s₂ → Set.EqOn f₁ f₂ s₁
The theorem `Set.EqOn.mono` states that for any two types `α` and `β`, two sets `s₁` and `s₂` of type `α`, and two functions `f₁` and `f₂` from `α` to `β`, if `s₁` is a subset of `s₂` and the functions `f₁` and `f₂` are equal on `s₂` (meaning that for each element `x` in `s₂`, `f₁(x)` is equal to `f₂(x)`), then `f₁` and `f₂` are also equal on `s₁`. In other words, the equality of two functions on a larger set implies their equality on any subset of that set.
More concisely: If `s₁ ⊆ s₂`, `f₁ : α → β`, `f₂ : α → β`, and `∀ x ∈ s₂, f₁ x = f₂ x`, then `∀ x ∈ s₁, f₁ x = f₂ x`.
|
Equiv.invOn
theorem Equiv.invOn :
∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α} {t : Set β}, Set.InvOn (⇑e) (⇑e.symm) t s
This theorem states that for any two types, `α` and `β`, and any equivalence `e` between `α` and `β`, if `s` is a set of type `α` and `t` is a set of type `β`, then the function `e` (viewed as mapping from `α` to `β`), and its inverse `e.symm` (viewed as mapping from `β` to `α`) are inverses of each other with respect to the sets `s` and `t`. This means that the function `e` and its inverse `e.symm` are left and right inverses when restricted to these sets. In other words, applying `e` followed by `e.symm` (or vice versa) will leave any element of the sets `s` and `t` unchanged.
More concisely: For any equivalence `e` between types `α` and `β`, and sets `s` of type `α` and `t` of type `β`, `e` and `e.symm` are mutual inverses when restricted to `s` and `t`, i.e., `e (x : s) ∈ t` if and only if `e.symm (y : t) = x`.
|
StrictMonoOn.restrict
theorem StrictMonoOn.restrict :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMonoOn f s → StrictMono (s.restrict f)
The theorem `StrictMonoOn.restrict` states that for any type `α` and `β` with a `Preorder` relation, and for any function `f` from `α` to `β`, if `f` is strictly monotone on a subset `s` of `α` (meaning for all `a, b` in `s`, `a < b` implies `f(a) < f(b)`), then the restriction of `f` to `s` is strictly monotone in its entire domain. In other words, if `f` preserves the strict order within `s`, it also preserves the strict order when restricted to `s`.
More concisely: If `f` is a strictly monotone function from a subset `s` of a preordered type `α` to another preordered type `β`, then the restriction of `f` to `s` is strictly monotone.
|
Set.BijOn.symm
theorem Set.BijOn.symm :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {g : β → α},
Set.InvOn f g t s → Set.BijOn f s t → Set.BijOn g t s
This theorem states that for any two sets `s` and `t` of types `α` and `β` respectively, with maps `f` from `α` to `β` and `g` from `β` to `α`, if `f` is an inverse of `g` on the range `t` and domain `s`, and `f` is a bijection from `s` to `t`, then `g` is a bijection from `t` to `s`. Here, a bijection is a function that is both injective (no two different inputs map to the same output) and surjective (every element of the target set is an output of the function).
More concisely: If functions `f` from set `s` to `t` and `g` from `t` to `s` are mutually inverse bijections, then each is a bijection between `s` and `t`.
|
Set.BijOn.mapsTo
theorem Set.BijOn.mapsTo :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → Set.MapsTo f s t
The theorem `Set.BijOn.mapsTo` states that for any types `α` and `β`, any sets `s` of `α` and `t` of `β`, and any function `f` from `α` to `β`, if `f` is a bijective function from `s` to `t` (meaning that `f` is injective on `s` and the image of `s` under `f` is exactly `t`), then `f` maps every element of `s` to some element in `t`. In other words, the image of the set `s` under the function `f` is contained in the set `t`.
More concisely: If `f` is a bijection from set `s` to set `t`, then the image of `s` under `f` is exactly `t`.
|
Set.MapsTo.nonempty
theorem Set.MapsTo.nonempty :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s t → s.Nonempty → t.Nonempty
The theorem `Set.MapsTo.nonempty` states that for any types `α` and `β`, and any sets `s` of `α` and `t` of `β`, and any function `f` from `α` to `β`, if `f` maps the elements of `s` into `t` (i.e., `Set.MapsTo f s t`), and if `s` is non-empty (i.e., `s.Nonempty`), then `t` must also be non-empty (i.e., `t.Nonempty`). In simple terms, this theorem says that if a function `f` maps a non-empty set `s` to a set `t`, then set `t` cannot be empty.
More concisely: If `f: α -> β` maps a non-empty set `s: Set α` to a set `t: Set β`, then `t` is non-empty.
|
Set.restrict_dite_compl
theorem Set.restrict_dite_compl :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : (x : α) → Decidable (x ∈ s)] (f : (a : α) → a ∈ s → β)
(g : (a : α) → a ∉ s → β), (sᶜ.restrict fun a => if h : a ∈ s then f a h else g a h) = fun a => g ↑a ⋯
This theorem states that for any set `s` of elements of type `α`, and any two functions `f` and `g` that map elements of `α` into a type `β` based on their membership in `s`, if we restrict the function that applies `f` to elements in `s` and `g` to elements not in `s` to the complement of `s`, we obtain a function equivalent to `g` when applied to the elements of `s`. In other words, when we're considering elements outside of `s` (`s` complement), we can effectively ignore the part of the function that applies to elements inside `s`; we're only concerned with `g`. Note that this is under the assumption that it can be decided for any element `x` of type `α` whether `x` is in `s` or not.
More concisely: For any set `s` and functions `f` and `g` from a type `α` to a type `β`, if `x ∈ s` implies `f x = g x`, then the restrictions of `f` and `g` to the complement of `s` are equal.
|
StrictMonoOn.mono
theorem StrictMonoOn.mono :
∀ {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
StrictMonoOn f s → s₂ ⊆ s → StrictMonoOn f s₂
This theorem states that if a function `f` is strictly monotone on a set `s` and if another set `s₂` is a subset of `s`, then the function `f` is also strictly monotone on `s₂`. Here, strict monotonicity means that for all pairs of distinct elements `a` and `b` belonging to the set such that `a < b`, we have `f(a) < f(b)`. The theorem therefore asserts the preservation of strict monotonicity under taking subsets.
More concisely: If `f` is a strictly monotone function on set `s`, then `f` is also strictly monotone on any subset `s₂` of `s`.
|
Set.SurjOn.subset_range
theorem Set.SurjOn.subset_range :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.SurjOn f s t → t ⊆ Set.range f
The theorem `Set.SurjOn.subset_range` states that for all types `α` and `β`, for any set `s` of type `α`, any set `t` of type `β`, and any function `f` from `α` to `β`, if `f` is surjective from `s` to `t` (i.e., every element of `t` is an image of some element of `s` under `f`), then the set `t` is a subset of the range of `f`. In other words, all elements of `t` are the images of some elements under the function `f`, without any restriction to `s`.
More concisely: If a function from type `α` to type `β` is surjective, then the image of the function contains the entire codomain `β`, i.e., `image f ⊆ β`.
|
Function.invFunOn_pos
theorem Function.invFunOn_pos :
∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] {s : Set α} {f : α → β} {b : β},
(∃ a ∈ s, f a = b) → Function.invFunOn f s b ∈ s ∧ f (Function.invFunOn f s b) = b
The theorem `Function.invFunOn_pos` states that for any types `α` and `β` (with `α` being nonempty), a set `s` of type `α`, a function `f` from `α` to `β`, and an element `b` of type `β`, if there exists an element `a` in set `s` such that `f(a) = b`, then the inverse function of `f` on `s` evaluated at `b` is an element of `s` and applying `f` to this inverse function evaluated at `b` gives `b` back. In simpler terms, the theorem asserts that the inverse function is a right inverse of `f` on its image under `f` in the set `s`.
More concisely: For any nonempty type `α`, set `s` of `α`, function `f` from `α` to `β`, and `b` in `β`, if `f(a) = b` for some `a` in `s`, then `(f.inv | s).(b) = a` and `f((f.inv | s).(b)) = b`.
|
Set.InjOn.eq_iff
theorem Set.InjOn.eq_iff :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {x y : α},
Set.InjOn f s → x ∈ s → y ∈ s → (f x = f y ↔ x = y)
This theorem states that for any sets `α` and `β` with `s` as a subset of `α`, and any function `f` from `α` to `β`, and any elements `x` and `y` from `α`, if `f` is injective on `s`, and both `x` and `y` are elements of `s`, then `f(x)` equals `f(y)` if and only if `x` equals `y`. In more mathematical terms, it expresses the property of an injective function where distinct inputs from a certain set produce distinct outputs.
More concisely: If `f` is an injective function from set `α` to set `β` and `x`, `y` are elements of subset `s` of `α`, then `f(x) = f(y)` if and only if `x = y`.
|
Set.BijOn.injOn
theorem Set.BijOn.injOn :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → Set.InjOn f s
This theorem states that for any two types `α` and `β`, and any sets `s` of type `α` and `t` of type `β`, and any function `f` that maps `α` to `β`, if `f` is bijective from set `s` to set `t`, then `f` is also injective on set `s`. In mathematical terms, if a function `f` is bijective (both injective and surjective) from one set to another, it is guaranteed to be injective (no two different elements in the domain map to the same element in the co-domain) on the domain set.
More concisely: If a function between two sets is bijective, then it is injective.
|
Set.restrict_eq
theorem Set.restrict_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), s.restrict f = f ∘ Subtype.val := by
sorry
The theorem `Set.restrict_eq` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any set `s` of elements from `α`, the restriction of `f` to `s`, denoted by `Set.restrict s f`, is equal to the composition of `f` and `Subtype.val`. In other words, restricting a function's domain to a subset and extracting the underlying element from a subtype yield the same result when applied to an element of the subtype. This theorem reflects the fact that restricting the domain of a function to a subset doesn't change the behavior of the function on that subset.
More concisely: For any type `α`, set `s ⊆ α`, function `f : α → β`, and `x ∈ s`, `Set.restrict s f x = f (Subtype.val x)`.
|
Set.mapsTo_empty
theorem Set.mapsTo_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : Set β), Set.MapsTo f ∅ t
The theorem `Set.mapsTo_empty` states that for any types `α` and `β`, and for any function `f` mapping `α` to `β` and any set `t` of type `β`, the function `f` maps the empty set to `t`. This is based on the definition of `Set.MapsTo`, which means that the image of every element from the first set is contained in the second set. Since the empty set has no elements, it trivially holds that all its elements (of which there are none) have their images in `t` under function `f`.
More concisely: For any functions `f: α → β` and sets `t: Set β`, the empty set of `α` maps to `t` under `f`, that is, `∅.map f = {}`.
|
Set.piecewise_op
theorem Set.piecewise_op :
∀ {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
{δ' : α → Sort u_7} (h : (i : α) → δ i → δ' i),
(s.piecewise (fun x => h x (f x)) fun x => h x (g x)) = fun x => h x (s.piecewise f g x)
The theorem `Set.piecewise_op` states that for any type `α`, any set `s` of type `α`, any two functions `f` and `g` from `α` to another type `δ` (which can itself depend on `α`), and any function `h` from `α` and `δ` to yet another type `δ'` (which can also depend on `α`), applying `h` to the function `Set.piecewise s f g` is the same as applying `Set.piecewise s` to `h` composed with `f` on `s` and `h` composed with `g` on the complement of `s`. In other words, we can "pull out" the function `h` from the piecewise defined function. This assumes that for each element in `α`, we can decide whether it is in `s` or not.
More concisely: For any set `s` in type `α`, functions `f` and `g` from `α` to type `δ`, and function `h` from `α × δ` to type `δ'`, we have `h (Set.piecewise s f g) = Set.piecewise s (λ x, h (x, f x)) (λ x, h (x, g x))`.
|
Set.SurjOn.mono
theorem Set.SurjOn.mono :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
s₁ ⊆ s₂ → t₁ ⊆ t₂ → Set.SurjOn f s₁ t₂ → Set.SurjOn f s₂ t₁
This theorem states that for any two types `α` and `β`, given two sets `s₁` and `s₂` of type `α`, two sets `t₁` and `t₂` of type `β`, and a function `f` from `α` to `β`, if `s₁` is a subset of `s₂` and `t₁` is a subset of `t₂`, and if `f` is surjective from `s₁` onto `t₂`, then `f` is also surjective from `s₂` onto `t₁`. In other words, if the function `f` maps all elements of `s₁` onto elements in `t₂`, then it also maps all elements of the larger set `s₂` onto elements in the smaller set `t₁`.
More concisely: If `f` is a surjective function from subset `s₁` of type `α` to subset `t₂` of type `β`, and `s₁` is a subset of `s₂`, then `f` is surjective from `s₂` to `t₁`.
|
Set.MapsTo.restrict_inj
theorem Set.MapsTo.restrict_inj :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t),
Function.Injective (Set.MapsTo.restrict f s t h) ↔ Set.InjOn f s
The theorem `Set.MapsTo.restrict_inj` states that for any given types `α` and `β`, any set `s` of type `α`, any set `t` of type `β`, and a function `f` from `α` to `β` that maps `s` onto `t`, the function `f` is injective on the restriction of `f` to `s` and `t` if and only if `f` is injective on `s`. This means that if for any two elements in `s`, their images under `f` are the same if and only if the elements themselves are the same, then the same property holds true when we restrict `f` to the elements in `s` that are mapped to `t`.
More concisely: If a function from type `α` to type `β` maps a set `s` of type `α` onto a set `t` of type `β` and is injective on `s`, then it is injective on the restriction of `s` to the elements in `t`.
|
Set.restrictPreimage_injective
theorem Set.restrictPreimage_injective :
∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
Function.Injective f → Function.Injective (t.restrictPreimage f)
The theorem `Set.restrictPreimage_injective` states that for all types `α` and `β`, given a set `t` of type `β` and a function `f` from `α` to `β`, if the function `f` is injective (meaning that it maps distinct inputs to distinct outputs), then the restriction of the function `f` onto the preimage of the set `t` is also injective. In mathematical terms, if $f: \alpha \rightarrow \beta$ is an injective function and $t$ is a set of elements of $\beta$, then the restriction of $f$ onto $f^{-1}(t)$ is also injective.
More concisely: If `f` is an injective function from type `α` to type `β` and `t` is a set of type `β`, then the restriction of `f` to `f⁻¹(t)` is also an injective function.
|
Set.piecewise_eq_of_not_mem
theorem Set.piecewise_eq_of_not_mem :
∀ {α : Type u_1} {δ : α → Sort u_6} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)] {i : α},
i ∉ s → s.piecewise f g i = g i
This theorem states that for any type `α`, a set `s` of elements of that type, and two functions `f` and `g` mapping elements of `α` to some type `δ`, along with a decidable instance for determining set membership, if a particular element `i` of type `α` does not belong to the set `s`, then applying the `piecewise` function of the set `s` to `f` and `g` at `i` is equivalent to applying `g` at `i`. In more mathematical terms, for some $i \notin s$, we have $s.piecewise(f, g)(i) = g(i)$.
More concisely: For any set `s` of type `α`, and functions `f` and `g` from `α` to some type `δ` with a decidable membership relation, if `i ∉ s`, then `s.piecewise f g i = g i`.
|
StrictMono.of_restrict
theorem StrictMono.of_restrict :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
StrictMono (s.restrict f) → StrictMonoOn f s
The theorem `StrictMono.of_restrict` states that for any given types `α` and `β` with preorders, a set `s` of type `α`, and a function `f` from `α` to `β`, if `f` is strictly monotone when its domain is restricted to the set `s` (i.e., `StrictMono (Set.restrict s f)`), then `f` is strictly monotone on the set `s` (i.e., `StrictMonoOn f s`). In more intuitive terms, if a function is strictly increasing when we only consider the values in a particular set, then the function is strictly increasing on that set.
More concisely: If a function restricted to a set is strictly monotone, then it is strictly monotone on that set.
|
Set.BijOn.inter_mapsTo
theorem Set.BijOn.inter_mapsTo :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
Set.BijOn f s₁ t₁ → Set.MapsTo f s₂ t₂ → s₁ ∩ f ⁻¹' t₂ ⊆ s₂ → Set.BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)
The theorem `Set.BijOn.inter_mapsTo` states that for any types `α` and `β`, any sets `s₁` and `s₂` of type `α`, any sets `t₁` and `t₂` of type `β`, and any function `f` from `α` to `β`, if `f` is bijective from `s₁` to `t₁` and `f` maps `s₂` to `t₂`, where the intersection of `s₁` and the pre-image of `t₂` under `f` is a subset of `s₂`, then `f` is bijective from the intersection of `s₁` and `s₂` to the intersection of `t₁` and `t₂`. In simpler terms, under these conditions, the function `f` preserves bijections when restricting to the intersections of its original domain and range sets.
More concisely: If `f` is a bijective function from `s₁` to `t₁`, `s₂ ⊆ f⁁⁻¹(t₂)`, and `f(s₁) = t₂`, then `f` is bijective from `s₁ ∩ s₂` to `t₁ ∩ t₂`.
|
Set.EqOn.comp_eq
theorem Set.EqOn.comp_eq :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_6} {f : ι → α} {g₁ g₂ : α → β},
Set.EqOn g₁ g₂ (Set.range f) → g₁ ∘ f = g₂ ∘ f
The theorem `Set.EqOn.comp_eq` states that for any types `α`, `β`, `ι`, any function `f : ι → α`, and any functions `g₁, g₂ : α → β`, if `g₁` and `g₂` are equal on the range of `f`, then the composition `g₁ ∘ f` is equal to the composition `g₂ ∘ f`. In other words, if two functions produce the same output for all inputs in the range of a third function, then their compositions with the third function are also equal.
More concisely: If functions `g₁` and `g₂` agree on the image of `f`, then `g₁ ∘ f` equals `g₂ ∘ f`.
|
Set.MapsTo.restrict_eq_codRestrict
theorem Set.MapsTo.restrict_eq_codRestrict :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t),
Set.MapsTo.restrict f s t h = Set.codRestrict (s.restrict f) t ⋯
This theorem states that for any two types `α` and `β`, any two sets `s : Set α` and `t : Set β`, and any function `f : α → β`, if the function `f` maps `s` into `t` (i.e., `Set.MapsTo f s t` is true), then the function obtained by restricting `f` to `s` and `t`, i.e., `Set.MapsTo.restrict f s t h`, is equivalent to the function obtained by restricting the codomain of the function `(s.restrict f)` to `t`, i.e., `Set.codRestrict (s.restrict f) t`. In other words, both methods of restricting the function `f` yield the same result.
More concisely: For any types `α`, `β`, sets `s : Set α`, `t : Set β`, and function `f : α → β`, if `Set.MapsTo f s t` holds, then `Set.MapsTo.restrict f s t` is equivalent to `Set.codRestrict (s.restrict f) t`.
|
Set.EqOn.image_eq
theorem Set.EqOn.image_eq :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β}, Set.EqOn f₁ f₂ s → f₁ '' s = f₂ '' s
The theorem `Set.EqOn.image_eq` states that for any set `s` of elements from a type `α`, and any two functions `f₁` and `f₂` from `α` to another type `β`, if `f₁` and `f₂` are equal on `s` (meaning `f₁ x = f₂ x` for all `x` in `s`), then the images of `s` under `f₁` and `f₂` are equal. In other words, applying either `f₁` or `f₂` to every element of `s` produces the same set of results.
More concisely: If two functions from a set to another type are equal on that set, then their images are equal.
|
Function.Bijective.bijOn_univ
theorem Function.Bijective.bijOn_univ :
∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Bijective f → Set.BijOn f Set.univ Set.univ
This theorem, referred to as the 'alias' of the forward direction of `Set.bijective_iff_bijOn_univ`, states that for any types `α` and `β` and any function `f` mapping `α` to `β`, if `f` is bijective, then `f` also exhibits a bijection between the universal set of `α` and the universal set of `β`. In simpler terms, a bijective function maps all elements of one set precisely to all elements of another set, including when those sets are the set of all elements of a given type.
More concisely: A bijective function between types `α` and `β` induces a bijection between their respective universal sets.
|
Set.BijOn.surjOn
theorem Set.BijOn.surjOn :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → Set.SurjOn f s t
This theorem states that for any two types `α` and `β`, and any sets `s` in `α` and `t` in `β`, if a function `f` from `α` to `β` is bijective on `s` to `t`, then the function `f` is also surjective from `s` to `t`. In other words, if a function `f` is both injective on `s` (every element of `s` maps to a unique element of `t`) and its image equals `t` (every element of `t` comes from an element of `s`), then every element of `t` definitely comes from an element of `s`, which is the definition of surjectivity. The proof is not shown here.
More concisely: If a function between two types is bijective on two sets, then it is surjective on one set onto the other.
|
Set.SurjOn.rightInvOn_invFunOn
theorem Set.SurjOn.rightInvOn_invFunOn :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [inst : Nonempty α],
Set.SurjOn f s t → Set.RightInvOn (Function.invFunOn f s) f t
The theorem `Set.SurjOn.rightInvOn_invFunOn` asserts that for any sets `s` of type `α` and `t` of type `β`, and any function `f` from `α` to `β`, if `α` is nonempty and `f` is surjective from `s` to `t` (that is, `t` is contained within the image of `s` under `f`), then the function `Function.invFunOn f s`, which constructs the inverse for `f` on the domain `s`, is a right inverse to `f` on `t` (meaning that `f (Function.invFunOn f s x) = x` for all `x` in `t`). In other words, this theorem is a formalization of the mathematical concept that a surjective function has a right inverse.
More concisely: If `f` is a surjective function from a nonempty set `s` to `t`, then there exists a function `g` such that `f(g(x)) = x` for all `x` in `t`.
|
Set.piecewise_eqOn_compl
theorem Set.piecewise_eqOn_compl :
∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] (f g : α → β),
Set.EqOn (s.piecewise f g) g sᶜ
This theorem states that for any type `α` and `β`, and for any set `s` of type `α`, a decidable property that a particular `α` is in `s`, and any two functions `f` and `g` from `α` to `β`, the function produced by the `Set.piecewise` function, which is `f` on the set `s` and `g` on its complement, is equal to `g` on the complement of `s`. In simple terms, it says that for any element not in `s`, the `Set.piecewise` function acts the same as the function `g`.
More concisely: For any type `α`, set `s` of `α`, decidable `P : α → Prop`, and functions `f : α → β` and `g : α → β`, the function `Set.piecewise s P f g` equals `g` on the complement of `s`.
|
Set.surjective_iff_surjOn_univ
theorem Set.surjective_iff_surjOn_univ :
∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f ↔ Set.SurjOn f Set.univ Set.univ
The theorem `Set.surjective_iff_surjOn_univ` states that for any function `f` from type `α` to type `β`, the function `f` is surjective if and only if `f` is surjective on the universal set of `α` to the universal set of `β`. In other words, a function is surjective if every element of type `β` is an image of some element of type `α`, which is equivalent to saying that the image of the entire set of type `α` under function `f` includes all elements of type `β`.
More concisely: A function between types is surjective if and only if its image under the universal map from the source type to the universe includes the universal map from the target type to the universe.
|
Set.LeftInvOn.injOn
theorem Set.LeftInvOn.injOn :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f₁' : β → α}, Set.LeftInvOn f₁' f s → Set.InjOn f s := by
sorry
This theorem states that for any types `α` and `β`, any set `s` of type `α`, and any two functions `f` and `f₁'` from `α` to `β` and `β` to `α` respectively, if `f₁'` is a left inverse to `f` on `s` (meaning that for any `x` in `s`, `f₁'(f(x))` equals `x`), then `f` is injective on `s`. That is, for any two elements `x₁` and `x₂` in `s`, if `f(x₁)` equals `f(x₂)`, then `x₁` must equal `x₂`. This essentially says that if a function `f` has a left inverse on a set, it can't map two different elements of the set to the same value.
More concisely: If a function `f` from type `α` to type `β` has a left inverse on a set `s` of type `α`, then `f` is injective on `s` (i.e., for any `x₁, x₂` in `s`, `x₁ = x₂` implies `f(x₁) = f(x₂)`).
|
Set.MapsTo.iterate
theorem Set.MapsTo.iterate :
∀ {α : Type u_1} {f : α → α} {s : Set α}, Set.MapsTo f s s → ∀ (n : ℕ), Set.MapsTo f^[n] s s
The theorem `Set.MapsTo.iterate` states that for any type `α`, a function `f` from `α` to `α`, and a set `s` of type `α`, if `f` maps `s` to itself (`Set.MapsTo f s s`), then for any natural number `n`, the `n`-times iterated function `f^[n]` also maps `s` to itself. In other words, applying `f` repeatedly `n` times to any element in `s` will result in an element that also belongs to `s`.
More concisely: If a function maps a set to itself, then the `n`-th power of the function also maps the set to itself for any natural number `n`.
|
Function.invFunOn_apply_eq
theorem Function.invFunOn_apply_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] {s : Set α} {f : α → β} {a : α},
a ∈ s → f (Function.invFunOn f s (f a)) = f a
This theorem states that for any types `α` and `β`, along with a nonempty instance of `α`, a set `s` of elements of type `α`, a function `f` mapping `α` to `β`, and an element `a` of type `α`, if `a` is in the set `s`, then applying the function `f` to the inverse of function `f` on the set `s` evaluated at `f(a)` gives `f(a)`. In other words, if `a` is in `s`, then the inverse function on `s` is truly a right inverse of `f` at `f(a)`. This means that applying `f` to the result of applying the inverse of `f` to `f(a)` leads us back to `f(a)`.
More concisely: For any sets `S` of type `α`, function `f : α → β`, and `a : α` in `S`, `f (invFunOnS a) = f a`, where `invFunOnS` is the inverse function of `f` restricted to `S`.
|
Set.InjOn.ne
theorem Set.InjOn.ne :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {x y : α},
Set.InjOn f s → x ∈ s → y ∈ s → x ≠ y → f x ≠ f y
This theorem, `Set.InjOn.ne`, states that for any two elements `x` and `y` of a set `s` of type `α`, and a function `f` from `α` to another type `β`, if `f` is injective on the set `s`, then whenever `x` and `y` are distinct elements of `s`, their images under `f` are also distinct. In mathematical terms, if $x$ and $y$ are different elements in a set $S$, and $f$ is a function such that $f: S \to T$, and $f$ is injective, then $f(x)$ and $f(y)$ are also different.
More concisely: If `f` is an injective function from set `s` of type `α` to type `β`, then distinct elements `x` and `y` in `s` have distinct images under `f`.
|
Mathlib.Data.Set.Function._auxLemma.1
theorem Mathlib.Data.Set.Function._auxLemma.1 :
∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, (a1 = a2) = (↑a1 = ↑a2)
This theorem states that for any type `α`, any property `p` on `α`, and any two elements `a1` and `a2` of the subtype of `α` consisting of elements satisfying `p`, the equality of `a1` and `a2` is equivalent to the equality of their underlying elements in `α`. In more mathematical terms, if we have two elements of a subset defined by some property `p` of a set `α`, then the elements are equal in the subset if and only if they are equal in the set `α`.
More concisely: For any type `α` and property `p` on `α`, two elements `a1` and `a2` of the subtype of elements satisfying `p` are equal if and only if their underlying elements in `α` are equal.
|
Set.injOn_of_injective
theorem Set.injOn_of_injective :
∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), Set.InjOn f s
This theorem states that for any two types `α` and `β`, and any function `f` from `α` to `β`, if the function `f` is injective (meaning that if `f x = f y` then `x = y`), then `f` is also injective on any subset `s` of `α`. In other words, the restriction of the function `f` to the subset `s` retains the injective property. This is expressed formally as `Set.InjOn f s`, meaning for any two elements `x₁` and `x₂` in the subset `s`, if `f x₁ = f x₂` then `x₁ = x₂`.
More concisely: If `f` is an injective function from type `α` to type `β`, then `f` restriction to any subset `s` of `α` remains injective.
|
Set.LeftInvOn.mono
theorem Set.LeftInvOn.mono :
∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : α → β} {f' : β → α},
Set.LeftInvOn f' f s → s₁ ⊆ s → Set.LeftInvOn f' f s₁
The theorem `Set.LeftInvOn.mono` states that for any types `α` and `β`, any sets `s` and `s₁` of `α`, and any functions `f : α → β` and `f' : β → α`, if `f'` is a left inverse to `f` on `s` (i.e., `f'(f(x)) = x` for all `x` in `s`), and `s₁` is a subset of `s`, then `f'` is also a left inverse to `f` on `s₁`. This means that the property of being a left inverse is preserved under taking subsets.
More concisely: If `f : α → β`, `f' : β → α`, `s ⊆ α`, `f'` is a left inverse to `f` on `s`, then `f'` is a left inverse to `f` on `s₁`.
|
Set.eqOn_empty
theorem Set.eqOn_empty : ∀ {α : Type u_1} {β : Type u_2} (f₁ f₂ : α → β), Set.EqOn f₁ f₂ ∅
The theorem `Set.eqOn_empty` states that for any two functions `f₁` and `f₂` that map from a type `α` to a type `β`, these two functions are equal on an empty set. In other words, no matter what the functions `f₁` and `f₂` are, they are considered equal on the empty set because there are no elements in the set for which they could potentially differ.
More concisely: For any functions `f₁ : α → β` and `f₂ : α → β` over types `α` and `β`, `f₁ = f₂` holds on the empty set `∅`.
|
Set.InjOn.comp
theorem Set.InjOn.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g : β → γ},
Set.InjOn g t → Set.InjOn f s → Set.MapsTo f s t → Set.InjOn (g ∘ f) s
The theorem `Set.InjOn.comp` states that for all types `α`, `β`, and `γ`, and for all sets `s` of `α` and `t` of `β`, if a function `g` from `β` to `γ` is injective on `t`, a function `f` from `α` to `β` is injective on `s`, and the image of `s` under `f` is contained in `t` (i.e., `f` maps `s` to `t`), then the composition of `g` and `f`, `g ∘ f`, is injective on `s`. In other words, the injectivity of individual functions and their mapping properties allow us to conclude the injectivity of their composition.
More concisely: If `f` maps a set `s` to a subset `t` of its image under an injective function `g`, and `f` and `g` are injective, then their composition `g ∘ f` is injective on `s`.
|
Set.mapsTo'
theorem Set.mapsTo' :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s t ↔ f '' s ⊆ t
The theorem `Set.mapsTo'` asserts that for any types `α` and `β`, any sets `s` of `α` and `t` of `β`, and any function `f` from `α` to `β`, the statement that `f` maps `s` into `t` is equivalent to the statement that the image of `s` under `f` is a subset of `t`. In other words, it says that every element of `s` gets mapped by `f` into an element in `t` if and only if all elements in the image of `s` under `f` are also elements of `t`.
More concisely: For any types α and β, sets s of α and t of β, and function f : α → β, the sets {x ∈ s | f x ∈ t} and f["s"] are equal.
|
Set.injOn_iff_injective
theorem Set.injOn_iff_injective :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s ↔ Function.Injective (s.restrict f) := by
sorry
This theorem states that for any type `α`, type `β`, a set `s` of type `α`, and a function `f` from `α` to `β`, the function `f` is injective on the set `s` if and only if the restriction of the function `f` to the set `s` is injective. Here, a function is said to be injective (or one-to-one) if it assigns a unique output to each unique input. In other words, if two values in the domain of the function map to the same value in the codomain, these two values must be the same. The theorem links the concept of injectivity to the concept of injectivity on a subset, asserting these are equivalent when considering a function restricted to a subset.
More concisely: For any function \(f : \alpha \rightarrow \beta\) and set \(s \subseteq \alpha\), \(f\) is injective on \(s\) if and only if the restriction \(f|_s : s \rightarrow \beta\) is injective.
|