Equiv.eq_image_iff_symm_image_eq
theorem Equiv.eq_image_iff_symm_image_eq :
∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β), t = ⇑e '' s ↔ ⇑e.symm '' t = s
This theorem states that for any two types `α` and `β`, given an equivalence `e` between `α` and `β`, and two sets `s` of type `α` and `t` of type `β`, the set `t` equals the image of `s` under the mapping `e` if and only if the image of `t` under the inverse mapping of `e` equals `s`. In other words, the images of the sets `s` and `t` under the mapping and its inverse, respectively, are equal if and only if the sets themselves are equal under the given equivalence.
More concisely: For any equivalence between types `α` and `β` and sets `s` of type `α` and `t` of type `β`, `s` and `t` are equal if and only if `t = e (s)` and `s = e⁻¹ (t)`, where `e` is the equivalence, `e (s)` is the image of `s` under `e`, and `e⁻¹ (t)` is the inverse image of `t` under `e`.
|
Set.image_equiv_eq_preimage_symm
theorem Set.image_equiv_eq_preimage_symm :
∀ {α : Type u_1} {β : Type u_2} (S : Set α) (f : α ≃ β), ⇑f '' S = ⇑f.symm ⁻¹' S
This theorem states that for any set `S` of type `α` and any bijective function `f` from `α` to another type `β`, the image of the set `S` under the function `f` (denoted as `⇑f '' S`) is equal to the preimage of the set `S` under the inverse of the function `f` (denoted as `⇑f.symm ⁻¹' S`). In other words, applying `f` to every element in `S` gives the same result as finding all the elements in `β` that get mapped back to `S` by the inverse of `f`.
More concisely: For any set `S` of type `α` and bijective function `f` from `α` to `β`, `f '' S = (f.symm)^-1 '' S`.
|
Equiv.image_eq_preimage
theorem Equiv.image_eq_preimage : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α), ⇑e '' s = ⇑e.symm ⁻¹' s := by
sorry
This theorem, named `Equiv.image_eq_preimage`, states that for any two types `α` and `β`, and an equivalence `e` between `α` and `β`, the image under `e` of a set `s` of type `α` is equal to the preimage under the inverse of `e` of the set `s`. In other words, applying the equivalence `e` to the elements of the set `s` results in the same set as one would obtain by finding all elements in type `β` that, under the inverse of the equivalence `e`, would be mapped to `s`.
More concisely: For any equivalence `e` between types `α` and `β` and set `s` of type `α`, the image of `s` under `e` equals the preimage of `s` under the inverse of `e`.
|
Equiv.ofLeftInverse.proof_1
theorem Equiv.ofLeftInverse.proof_1 : ∀ {α : Sort u_1} {β : Type u_2} (f : α → β) (a : α), ∃ y, f y = f a
This theorem states that for any function `f` mapping from a type `α` to a type `β` and for any element `a` belonging to type `α`, there exists an element `y` in type `α` such that the function `f` applied to `y` is equal to `f` applied to `a`. This theorem captures the possibility of having multiple elements in the domain mapping to the same element in the codomain, a characteristic feature of non-injective (or not one-to-one) functions.
More concisely: For any function `f` from type `α` to type `β` and any `a` in `α`, there exists `y` in `α` such that `f(y) = f(a)`.
|
Equiv.symm_image_image
theorem Equiv.symm_image_image : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α), ⇑e.symm '' (⇑e '' s) = s := by
sorry
The theorem `Equiv.symm_image_image` states that for any types `α` and `β`, and any equivalence relation `e` between `α` and `β`, and for any set `s` of type `α`, the image of the image of `s` under `e` and its inverse `e.symm` is equal to `s` itself. In other words, applying an equivalence transformation to a set and then the reverse transformation brings us back to the original set. This theorem is a formal restatement of the intuitive idea that equivalence transformations are reversible.
More concisely: For any equivalence relation `e` on types `α` and `β`, and any set `s` of type `α`, the image of `s` under `e` and then the image of that result under `e.symm` equals `s`.
|
Equiv.image_preimage
theorem Equiv.image_preimage : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set β), ⇑e '' (⇑e ⁻¹' s) = s
The theorem `Equiv.image_preimage` states that for any two types `α` and `β`, given an equivalence `e` between these types and a set `s` of type `β`, the image under `e` of the preimage under `e` of the set `s` is equal to `s` itself. In other words, if you first apply the inverse of `e` to `s` and then apply `e` to the result, you get back `s`. This theorem is a formal statement of the property that the composition of a function and its inverse yields the original input, in the context of set membership.
More concisely: For any equivalence relation `e` between types `α` and `β` and set `s` of type `β`, `e''(e⁻¹[s]) = s`. (Here, `e⁻¹[s]` denotes the preimage of `s` under `e`, and `e''` denotes the image of a set under `e`.)
|
Set.mem_image_equiv
theorem Set.mem_image_equiv :
∀ {α : Type u_1} {β : Type u_2} {S : Set α} {f : α ≃ β} {x : β}, x ∈ ⇑f '' S ↔ f.symm x ∈ S
This theorem states that for any types `α` and `β`, any set `S` of elements of type `α`, any bijection `f` from `α` to `β`, and any element `x` of type `β`, the element `x` is in the image of the set `S` under the function `f` if and only if the inverse of `x` under `f` is in the set `S`. In mathematical terms, we can say $x \in f(S) \iff f^{-1}(x) \in S$. This is a basic property about the interaction between function application, inverse functions, and set membership.
More concisely: For any sets S of type α, bijection f from α to β, and element x of type β, x is in the image of S under f if and only if the inverse image of x under f is in S. In symbolic form: x ∈ f(S) ↔ f⁻¹(x) ∈ S.
|
Equiv.preimage_image
theorem Equiv.preimage_image : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α), ⇑e ⁻¹' (⇑e '' s) = s
The theorem `Equiv.preimage_image` states that for all types `α` and `β`, and for every bijective function `e` from `α` to `β` and any set `s` of type `α`, the pre-image of the image of `s` under the function `e` equals to `s` itself. In other words, if you take a set `s`, map all of its elements to another type via a bijection `e`, and then map the resulting set back via the inverse of `e`, you will get the original set `s` back. This corresponds to the mathematical concept that the pre-image of the image of a set under a bijective function equals the original set.
More concisely: For every bijective function `e` from type `α` to type `β`, and any set `s` of type `α`, `e''(e(s)) = s`.
|
Set.preimage_equiv_eq_image_symm
theorem Set.preimage_equiv_eq_image_symm :
∀ {α : Type u_1} {β : Type u_2} (S : Set α) (f : β ≃ α), ⇑f ⁻¹' S = ⇑f.symm '' S
The theorem `Set.preimage_equiv_eq_image_symm` states that for any set `S` of type `α` and for any bijective mapping `f` between types `β` and `α`, the preimage of `S` under `f` is equal to the image of `S` under the inverse of `f`. In other words, if you perform the inverse operation of `f` on the set `S`, it is the same as applying `f` and then mapping `S` back to its original state. This is a property of bijective functions, where each element in both the domain and codomain pair up uniquely.
More concisely: For any bijective function $f : \beta \rightarrow \alpha$ and set $S \subseteq \alpha$, the preimage $f^{-1}(S)$ is equal to the image $f(S^{-1})$ under set inverse operations.
|
Equiv.image.proof_2
theorem Equiv.image.proof_2 : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (y : ↑(⇑e '' s)), e.symm ↑y ∈ s
This theorem states that for every two types `α` and `β`, if there exists a bijective function `e` from `α` to `β`, and `s` is a set of elements of type `α`, then for every element `y` that is in the image of `s` under the function `e`, the preimage of `y` under the inverse of `e` is an element of `s`. In simpler terms, if you take an element from the set `s`, apply the function `e`, and then apply the inverse of `e`, you will end up back in the original set `s`.
More concisely: If `e: α ↔ β` is a bijective function and `s ⊆ α` such that `y ∈ s'` where `y = e(x)` for some `x ∈ s`, then `e⁻¹(y) ∈ s`.
|
Equiv.image.proof_1
theorem Equiv.image.proof_1 : ∀ {α : Type u_2} {β : Type u_1} (e : α ≃ β) (s : Set α) (x : ↑s), e ↑x ∈ ⇑e '' s := by
sorry
This theorem states that for any two types `α` and `β`, and an equivalence `e` from `α` to `β`, given a set `s` of type `α` and any element `x` of the set `s`, the image of `x` under the equivalence `e` is in the image of the set `s` under `e`. In other words, if we map a set from one type to another using an equivalence, every element in the original set will also be in the image set after the mapping.
More concisely: For any equivalence `e` between types `α` and `β` and any set `s` of type `α`, for all `x ∈ s`, `e(x) ∈ s.image under e`.
|
Equiv.apply_ofInjective_symm
theorem Equiv.apply_ofInjective_symm :
∀ {α : Sort u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (b : ↑(Set.range f)),
f ((Equiv.ofInjective f hf).symm b) = ↑b
The theorem `Equiv.apply_ofInjective_symm` states that for any injective function `f` mapping from a type `α` to a type `β`, and for any element `b` in the range of `f`, the inverse of the equivalence derived from `f` (due to its injectiveness), when applied to `b`, will give back `b` when `f` is applied to it. In other words, if we consider the inverse mapping of `b` back to the domain of `f` and then reapply `f` to it, we will end up with the original `b`. It confirms the correctness of the inverse operation in the context of the constructed equivalence.
More concisely: For an injective function `f` from type `α` to type `β`, and for any `b` in the range of `f`, we have `f (Equiv.symm (Equiv.mk _ _ _ b)) = b`.
|
dite_comp_equiv_update
theorem dite_comp_equiv_update :
∀ {α : Type u_1} {β : Sort u_2} {γ : Sort u_3} {p : α → Prop} (e : β ≃ Subtype p) (v : β → γ) (w : α → γ) (j : β)
(x : γ) [inst : DecidableEq β] [inst_1 : DecidableEq α] [inst_2 : (j : α) → Decidable (p j)],
(fun i => if h : p i then Function.update v j x (e.symm ⟨i, h⟩) else w i) =
Function.update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x
This theorem states that for any types `α`, `β`, and `γ`, and a property `p` of the type `α`, an equivalence `e` from `β` to the subtype determined by `p`, and functions `v` from `β` to `γ` and `w` from `α` to `γ`, and elements `j` of `β` and `x` of `γ`, and given that `β` and `α` have decidable equality, and each `j` of type `α` has a decidable property `p`, the composition of an updated function with an equivalence on a subtype is equal to an updated function. Specifically, a function that for each `i` of type `α` returns an updated version of `v` at `j` if `p` holds for `i`, and `w i` otherwise, is equal to a function that, after being updated at the point `e j`, returns `v` applied to the inverse of `e` at `⟨i, h⟩` if `p` holds for `i`, and `w i` otherwise.
More concisely: For types `α`, `β`, and `γ`, given an equivalence `e` from `β` to a subtype of `α` determined by a decidable property `p`, functions `v: β → γ` and `w: α → γ`, and elements `j: β` and `x: γ`, if `β` and `α` have decidable equality and each element of `α` has decidable property `p`, then the function updating `v` with `w` using `p` equals the function updated at `e(j)` with `v` and `w`.
|
Equiv.symm_preimage_preimage
theorem Equiv.symm_preimage_preimage :
∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set β), ⇑e.symm ⁻¹' (⇑e ⁻¹' s) = s
The theorem `Equiv.symm_preimage_preimage` states that for any two types `α` and `β`, and any equivalence `e` between them, and any set `s` of elements of type `β`, the preimage under `e.symm` (the inverse of `e`) of the preimage under `e` of `s` is equal to `s`. This essentially means that applying an equivalence and its inverse in succession to a set leaves the set unchanged.
More concisely: For any equivalence $e : \alpha \cong \beta$ and set $s \subseteq \beta$, the preimages under the inverse $e.symm$ of $e(X)$ and $X$ are equal: $e.symm(e(s)) = s$.
|
Equiv.preimage_symm_preimage
theorem Equiv.preimage_symm_preimage :
∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α), ⇑e ⁻¹' (⇑e.symm ⁻¹' s) = s
This theorem, `Equiv.preimage_symm_preimage`, states that for any types `α` and `β`, given an equivalence `e` between `α` and `β`, and a set `s` of type `α`, the preimage of the preimage of `s` under the inverse of `e` is equal to `s` itself. Here, `⇑e` and `⇑e.symm` denote the function corresponding to the equivalence `e` and its inverse respectively, and `⁻¹'` denotes the preimage of a set. In mathematical terms, this means if you take a set in `α`, map it to `β` using the inverse of the equivalence, and then map it back to `α` using the equivalence, you end up with the set you started with.
More concisely: For any equivalence `e` between types `α` and `β` and any set `s` of type `α`, `s = (e.symm ^-1)' (e ^-1 s)`.
|
Equiv.ofInjective_symm_apply
theorem Equiv.ofInjective_symm_apply :
∀ {α : Sort u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (a : α),
(Equiv.ofInjective f hf).symm ⟨f a, ⋯⟩ = a
This theorem states that for any injective function `f` from a domain `α` to a codomain `β`, and for any element `a` in `α`, the inverse application of the equivalence between `α` and the range of `f` (which is guaranteed by the injectivity of `f`) to the element in the range of `f` equal to `f(a)` is equal to `a`. Essentially, it confirms that reversing the mapping of `f` through this equivalence will retrieve the original element from the domain `α`.
More concisely: For any injective function `f` from domain `α` to codomain `β`, `f. inverse (f (x)) = x` for all `x` in `α`.
|
Equiv.subset_image
theorem Equiv.subset_image :
∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β), ⇑e.symm '' t ⊆ s ↔ t ⊆ ⇑e '' s
The theorem `Equiv.subset_image` states that for any types `α` and `β` and any equivalence relation `e` from `α` to `β`, and for any sets `s` of type `α` and `t` of type `β`, the image of `t` under the inverse of `e` is a subset of `s` if and only if `t` itself is a subset of the image of `s` under `e`. This theorem is an alias of `Equiv.symm_image_subset`, showing the relationship between the image of a set under an equivalence relation and its inverse.
More concisely: For any equivalence relation `e` between types `α` and `β`, and sets `s` of type `α` and `t` of type `β`, `t ⊆ e.image s` if and only if `s ⊆ e.image t`.
|
Equiv.self_comp_ofInjective_symm
theorem Equiv.self_comp_ofInjective_symm :
∀ {α : Sort u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f),
f ∘ ⇑(Equiv.ofInjective f hf).symm = Subtype.val
The theorem `Equiv.self_comp_ofInjective_symm` states that for any injective function `f` from type `α` to type `β`, the composition of `f` and the inverse of the equivalence relation obtained from `f` being injective is equal to the subtype value function. In essence, this means that if `f` is an injective function, then applying `f` to the result of the inverse equivalence operation gives you the original element in the domain `α`, encapsulating the idea of retracing the steps of the injective function.
More concisely: For any injective function `f`: `f ∘ inv_eq_of_injective f = subtype.val`. Here, `inv_eq_of_injective f` denotes the inverse of the equivalence relation induced by `f`, and `subtype.val` is the value function for the subtype induced by `f`.
|
Equiv.subset_image'
theorem Equiv.subset_image' :
∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β), s ⊆ ⇑e.symm '' t ↔ ⇑e '' s ⊆ t
This theorem, referred to as `Equiv.subset_image'`, states that for any two types `α` and `β`, any equivalence `e` from `α` to `β`, and any sets `s` of type `α` and `t` of type `β`, the set `s` is a subset of the image of `t` under the inverse of `e` if and only if the image of `s` under `e` is a subset of `t`. In other words, it relates the subset relations between two sets under an equivalence and its inverse.
More concisely: For any equivalence between types `α` and `β` and sets `s` of type `α` and `t` of type `β`, `s ⊆ e. inverse ''t iff e ''s ⊆ t`.
|
Equiv.range_eq_univ
theorem Equiv.range_eq_univ : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), Set.range ⇑e = Set.univ
The theorem `Equiv.range_eq_univ` states that for any two types `α` and `β`, if there exists a bijection `e` between them (denoted as `α ≃ β`), then the range of `e` (i.e., the set of all images of elements in `α` under `e`) is the universal set of `β`. In other words, every element of `β` is an image of some element of `α` under the bijection `e`. This is a formalization of the idea that a bijection is a function that pairs elements from two sets such that every element in each set has a unique partner in the other set.
More concisely: If `α` and `β` are type-equivalent (`α ≃ β`), then the range of any bijection `e` between them equals the universe of `β`.
|