Function.Embedding.coeFn_mk
theorem Function.Embedding.coeFn_mk :
∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (i : Function.Injective f), ⇑{ toFun := f, inj' := i } = f
This theorem, `Function.Embedding.coeFn_mk`, states that for all types `α` and `β`, given a function `f` from `α` to `β` and a proof `i` that `f` is injective (meaning that if `f x = f y` then `x = y`), the function produced by the embedding `{ toFun := f, inj' := i }` is equal to the original function `f`. In math terms, if `f: α → β` is an injective function, then the function produced by the embedding using `f` as the function and the proof of its injectivity is exactly the same as `f`.
More concisely: For all types `α` and `β`, if `f: α → β` is an injective function and `i:` `Injective f`, then the embedding `{ toFun := f, inj' := i }` is equal to `f`.
|
Function.Embedding.inj'
theorem Function.Embedding.inj' : ∀ {α : Sort u_1} {β : Sort u_2} (self : α ↪ β), Function.Injective self.toFun := by
sorry
The theorem `Function.Embedding.inj'` states that for any two types `α` and `β`, any embedding from `α` to `β` is an injective function. In other words, if we have an embedding `self` from `α` to `β`, then the function represented by `self.toFun` is injective. Here, an injective function is defined as a function `f` from `α` to `β` such that for all values `a₁` and `a₂` in `α`, if `f(a₁)` equals `f(a₂)`, then `a₁` must be equal to `a₂`.
More concisely: For any embeddings `self : α → β` in Lean 4, the function `self.toFun` is injective.
|
Function.Embedding.injective
theorem Function.Embedding.injective : ∀ {α : Sort u_1} {β : Sort u_2} (f : α ↪ β), Function.Injective ⇑f
The theorem `Function.Embedding.injective` states that for all types `α` and `β`, any function `f` from `α` to `β` that is an embedding (denoted as `α ↪ β`) is also injective. Here, a function is called injective if applying the function to two equal elements from `α` (i.e., `f a₁ = f a₂`) implies that these elements were already equal in `α` (i.e., `a₁ = a₂`). In other words, an embedding function does not map distinct elements in `α` to the same element in `β`.
More concisely: An embedding function between types `α` and `β` is a injective function.
|
Function.Embedding.ext
theorem Function.Embedding.ext : ∀ {α : Sort u_1} {β : Sort u_2} {f g : α ↪ β}, (∀ (x : α), f x = g x) → f = g := by
sorry
This theorem states that for any two function embeddings `f` and `g` from a sort `α` to another sort `β`, if for every element `x` in sort `α` the result of function `f` applied to `x` is equal to the result of function `g` applied to `x`, then the functions `f` and `g` are equal. In other words, two function embeddings between the same sorts are the same if they produce the same output for every input.
More concisely: If two function embeddings from sort `α` to sort `β` agree on every element of `α`, then they are equal.
|