EquivLike.bijective_comp
theorem EquivLike.bijective_comp :
∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [iE : EquivLike E α β] (e : E) (f : β → γ),
Function.Bijective (f ∘ ⇑e) ↔ Function.Bijective f
The theorem `EquivLike.bijective_comp` states that for all types `E`, `α`, `β`, and `γ`, where `E` has an equivalence-like relationship with `α` and `β`, given an instance `e` of `E` and a function `f` from `β` to `γ`, the composition of `f` and `e` is a bijective function if and only if `f` itself is a bijective function. In other words, the bijectivity of `f` is preserved when it is composed with an equivalence-like object `e`.
More concisely: For any type `E` with an equivalence-relation `_≡_`, and functions `f : β → γ` and `e : α ≃ β` such that `e` is an equivalence-like relation, if `f` is bijective then so is `f ∘ e`.
|
EquivLike.right_inv
theorem EquivLike.right_inv :
∀ {E : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [self : EquivLike E α β] (e : E),
Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
The theorem `EquivLike.right_inv` states that for any types `E`, `α`, and `β`, and for any instance of the `EquivLike` structure between `α` and `β`, the coercion functions in both directions, `EquivLike.inv` and `EquivLike.coe`, are right inverses to each other. In other words, applying `EquivLike.coe` followed by `EquivLike.inv` to any element results in the original element, or formally, `(EquivLike.inv e) ∘ (EquivLike.coe e) = id`.
More concisely: For any type `α` and `β` with an `EquivLike` relationship, the coercion functions `EquivLike.coe` and `EquivLike.inv` satisfy `EquivLike.inv ∘ EquivLike.coe = id`.
|
EquivLike.bijective
theorem EquivLike.bijective :
∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : EquivLike E α β] (e : E), Function.Bijective ⇑e
The theorem `EquivLike.bijective` states that for any types `α`, `β` and `E` in given sorts, if there exists an `EquivLike` instance between `α` and `β` for the type `E`, then a function represented by the application of this `E` is bijective. In other words, this function is both injective (each element in the domain maps to a unique element in the codomain) and surjective (every element in the codomain is the image of at least one element in the domain).
More concisely: If `α` and `β` are types with an `EquivLike` relation `E` between them, then the function induced by `E` is a bijection.
|
EquivLike.inv_apply_apply
theorem EquivLike.inv_apply_apply :
∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : EquivLike E α β] (e : E) (a : α), EquivLike.inv e (e a) = a
This theorem, `EquivLike.inv_apply_apply`, states that for any types `E`, `α`, `β`, and any instance `iE` of `EquivLike` relationship between `E`, `α` and `β`, for any element `e` of `E` and `a` of `α`, applying `e` to `a` and then applying the inverse of `e` to the result will give back `a`. This is a generic form of the `Equiv.symm_apply_apply` theorem for `EquivLike` types, which are supposed to represent some form of equivalence relationship between different types. The theorem essentially asserts that the inverse operation undoes the effect of the original operation.
More concisely: For any type equivalences `EquivLike` between types `E`, `α`, and `β`, and any `e : E`, `a : α`, the equivalent elements `e a` and `e (e a)` hold. In other words, applying the inverse of an equivalence relation followed by the original relation results in the identity relation.
|
EquivLike.apply_inv_apply
theorem EquivLike.apply_inv_apply :
∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : EquivLike E α β] (e : E) (b : β), e (EquivLike.inv e b) = b
This theorem, named `EquivLike.apply_inv_apply`, essentially states that for any sort `E`, types `α` and `β`, and for any instance of `EquivLike` between `α` and `β`, given an element `e` of `E` and `b` of `β`, applying `e` to the inverse of `b` (under `e`) will yield `b` itself. This theorem is generally used in generic contexts when working with classes extending `EquivLike`. For specific isomorphism types like `Equiv`, you should use `Equiv.apply_symm_apply` or its equivalent. The theorem essentially encapsulates the idea that applying a function to its inverse will yield the original input, which is an important property in the theory of functions and isomorphisms.
More concisely: For any `EquivLike` equivalence relation `e` between types `α` and `β`, `e (e.inv x) = x` holds for all `x : β`.
|
EquivLike.coe_injective'
theorem EquivLike.coe_injective' :
∀ {E : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [self : EquivLike E α β] (e g : E),
EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
The theorem `EquivLike.coe_injective'` asserts that for any sort `E`, and any two types `α` and `β`, given an equivalence-like structure `EquivLike E α β`, the two coercion functions, `EquivLike.coe` and `EquivLike.inv`, are jointly injective. In other words, if two elements `e` and `g` of sort `E` have the same forward and backward coercion functions, then `e` and `g` must be the same. Essentially, this theorem states that the combination of forward and backward coercions uniquely identifies an element in `E`.
More concisely: Given an equivalence-like structure on types `α` and `β` over sort `E`, the forward and backward coercion functions are jointly injective, i.e., if `EquivLike.coe α e = EquivLike.coe α g` and `EquivLike.inv β (EquivLike.coe β x) = EquivLike.inv β (EquivLike.coe β y)`, then `e = g` and `x = y` in `E`.
|
EquivLike.subsingleton_dom
theorem EquivLike.subsingleton_dom :
∀ {F : Sort u_2} {β : Sort u_4} {γ : Sort u_5} [iF : EquivLike F β γ] [inst : Subsingleton β], Subsingleton F := by
sorry
This theorem states that for any sorts `F`, `β`, and `γ`, if there exists an equivalence relation (`EquivLike`) from `F` to `β` and `γ`, and if `β` is a subsingleton (a type with at most one element), then `F` is also a subsingleton. This is not made an instance to avoid slowing down every single `Subsingleton` typeclass search.
More concisely: If `F` is a sort, `EquivLike` is an equivalence relation from `F` to both `β` and `γ`, and `β` is a subsingleton, then `F` is a subsingleton.
|
EquivLike.surjective
theorem EquivLike.surjective :
∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : EquivLike E α β] (e : E), Function.Surjective ⇑e
The theorem `EquivLike.surjective` states that for any types `E`, `α`, and `β`, given that there exists an equivalence relation `iE` between `α` and `β` represented by `E`, then for any element `e` of type `E`, the function that applies `e` is surjective. In other words, every element in `β` is the image of some element in `α` under the function `e`.
More concisely: Given an equivalence relation `iE` between types `α` and `β` represented by `E`, the function that maps each equivalence class to its representative element is surjective.
|
EquivLike.comp_bijective
theorem EquivLike.comp_bijective :
∀ {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [iF : EquivLike F β γ] (f : α → β) (e : F),
Function.Bijective (⇑e ∘ f) ↔ Function.Bijective f
The theorem `EquivLike.comp_bijective` states that for any type `F`, and any types `α`, `β`, and `γ` with `EquivLike` relation between types `β` and `γ`, given a function `f` from `α` to `β` and an equivalence `e` of type `F`, the function `f` is bijective if and only if the composition of `f` with `e` (denoted as `⇑e ∘ f`) is bijective. Here, bijectiveness means that the function is both injective (it never maps different inputs to the same output) and surjective (every possible output is produced by at least one input). This theorem essentially asserts that composing a bijective function with an equivalence doesn't affect the bijectiveness of the function.
More concisely: For any type `F`, type `α`, and types `β` and `γ` with an `EquivLike` relation, if `f: α → β` is bijective and `e: F` is an equivalence from `β` to `γ`, then `f ∘ e` is also bijective.
|
EquivLike.left_inv
theorem EquivLike.left_inv :
∀ {E : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [self : EquivLike E α β] (e : E),
Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
The theorem `EquivLike.left_inv` states that for every type `E`, along with its associated types `α` and `β` such that `E` is an equivalence between `α` and `β`, the coercion functions in the forward and backward directions are left inverses of each other. In other words, if `e` is an object of type `E`, then composing the function `EquivLike.inv e` after `EquivLike.coe e`, and applying this composition to any input, always returns the original input. This is equivalent to saying that `EquivLike.inv e` undoes the action of `EquivLike.coe e`, or in mathematical notation, `(EquivLike.inv e) ∘ (EquivLike.coe e) = id`.
More concisely: For every equivalence `E` between types `α` and `β` in Lean, `EquivLike.inv (EquivLike.coe e) = id` for all objects `e` of type `E`.
|
EquivLike.injective
theorem EquivLike.injective :
∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [iE : EquivLike E α β] (e : E), Function.Injective ⇑e
This theorem states that for any types `E`, `α`, and `β`, if `E` has the structure of `EquivLike` (which is a typeclass encapsulating the properties of being equivalent) between `α` and `β`, then for any element `e` of type `E`, the function represented by `e` (denoted by `⇑e` or `coeFn e`) is injective. In other words, if `⇑e x = ⇑e y`, then it must be the case that `x = y`. This property is typical for functions that establish a one-to-one correspondence (or equivalence) between elements of two sets.
More concisely: If `E` is an equivalence relation between types `α` and `β` (an instance of `EquivLike E α β`), then the function `coeFn : E → α → β` represented by each equivalence `e` in `E` is an injection.
|