English
For an embedding f : α ↪ β, there is a computable inverse invOfMemRange : Set.range f → α, which returns the unique preimage a ∈ α for each element of the image, i.e., invOfMemRange(⟨f(a), proof⟩) = a.
Русский
Для вложения f : α ↪ β существует вычислимое обратное отображение invOfMemRange : Set.range f → α, которое возвращает уникальный предобразующий элемент a ∈ α для каждого элемента образа, то есть invOfMemRange(⟨f(a), доказательство⟩) = a.
LaTeX
$$$\\text{Let } f: \\alpha \\hookrightarrow \\beta. \\text{ Then } invOfMemRange: \\operatorname{range}(f) \\to \\alpha \\text{ is the inverse on the image.}$$$
Lean4
/-- The inverse of an embedding `f : α ↪ β`, of the type `↥(Set.range f) → α`.
This is the computable version of `Function.invFun` that requires `Fintype α` and `DecidableEq β`,
or the function version of applying `(Equiv.ofInjective f f.injective).symm`.
This function should not usually be used for actual computation because for most cases,
an explicit inverse can be stated that has better computational properties.
This function computes by checking all terms `a : α` to find the `f a = b`, so it is O(N) where
`N = Fintype.card α`.
-/
def invOfMemRange : α :=
f.injective.invOfMemRange b
