EmbeddingLike.injective'
theorem EmbeddingLike.injective' :
∀ {F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [inst : FunLike F α β]
[self : EmbeddingLike F α β] (f : F), Function.Injective ⇑f
The theorem `EmbeddingLike.injective'` asserts that for any types `F`, `α`, and `β`, given a term `f` of type `F` and assuming `F` is a `FunLike` from `α` to `β` and also an `EmbeddingLike` from `α` to `β`, the coercion of `f` to a function from `α` to `β` must be injective. In other words, if two elements of `α` are sent to the same element of `β` by this function, then these two elements must have been the same to start with. This theorem is a guarantee that the function produced by the coercion operation preserves distinctness of elements.
More concisely: Given a type `F` that is both a FunLike and an EmbeddingLike from `α` to `β`, the induced function from `α` to `β` by the coercion is injective.
|
EmbeddingLike.injective
theorem EmbeddingLike.injective :
∀ {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [inst : FunLike F α β] [i : EmbeddingLike F α β] (f : F),
Function.Injective ⇑f
This theorem states that for any types `F`, `α`, and `β`, if `F` is a `FunLike` type from `α` to `β` and an `EmbeddingLike` from `α` to `β`, then any term `f` of type `F` is injective. In other words, if `f` maps two elements of `α` to the same element of `β`, then these two elements were the same to begin with. This theorem, therefore, guarantees the injectivity of 'function-like' objects in a given context.
More concisely: If `F` is a functor and an embedding from type `α` to type `β`, then any term `f` of type `F α β` is an injection.
|
Mathlib.Data.FunLike.Embedding._auxLemma.1
theorem Mathlib.Data.FunLike.Embedding._auxLemma.1 :
∀ {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [inst : FunLike F α β] [i : EmbeddingLike F α β] (f : F) {x y : α},
(f x = f y) = (x = y)
The theorem `Mathlib.Data.FunLike.Embedding._auxLemma.1` states that for any types `F`, `α`, `β`, if `F` is function-like from `α` to `β`, and `F` has an embedding-like property from `α` to `β`, then for any function `f` of type `F` and any elements `x` and `y` of `α`, the equation `f(x) = f(y)` is equivalent to `x = y`. In simpler terms, it means that the function `f` preserves distinctness of elements, that is, if `x` and `y` are distinct, their images under `f` are also distinct, and vice versa. This is a formal way to express that the function `f` is injective.
More concisely: If `F` is a function-like type with an embedding-like property from type `α` to `β`, then `F` is an injection from `α` to `β`.
|