English
If f is injective, then there exists a map invOfMemRange: Set.range(f) → α that acts as a partial inverse of f on its range.
Русский
Если f инъективна, существует отображение invOfMemRange: Set.range(f) → α, которое является частичным обратным к f на области образа.
LaTeX
$$$ \\exists inv:\\mathrm{Set.range}(f) \\to \\alpha\\; (\\text{Injective}(f) \\Rightarrow \\operatorname{Inverse}(f, inv)) $$$
Lean4
/-- The inverse of an `hf : injective` function `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 hf).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 : Set.range f → α := fun b =>
Finset.choose (fun a => f a = b) Finset.univ
((existsUnique_congr (by simp)).mp (hf.existsUnique_of_mem_range b.property))
