English
Given a finite α and an embedding f: α ↪ β, there is a computable equivalence α ≃ Set.range f.
Русский
Для данного конечного α и вложения f: α ↪ β существует вычислимая эквивалентность α ≃ Set.range f.
LaTeX
$$$\text{toEquivRange} : α \simeq \mathrm{Set.range}(f)$$$
Lean4
/-- Computably turn an embedding `f : α ↪ β` into an equiv `α ≃ Set.range f`,
if `α` is a `Fintype`. Has poor computational performance, due to exhaustive searching in
constructed inverse. When a better inverse is known, use `Equiv.ofLeftInverse'` or
`Equiv.ofLeftInverse` instead. This is the computable version of `Equiv.ofInjective`.
-/
def toEquivRange : α ≃ Set.range f
where
toFun := fun a => ⟨f a, Set.mem_range_self a⟩
invFun := f.invOfMemRange
left_inv := fun _ => by simp
right_inv := fun _ => by simp
