English
An equivalence f : α ≃ β yields an embedding α ↪ β via toEmbedding.
Русский
Эквиваленция f : α ≃ β дает вложение α ↪ β через toEmbedding.
LaTeX
$$$\text{toEmbedding}(f):\alpha \hookrightarrow \beta$$$
Lean4
/-- Convert an `α ≃ β` to `α ↪ β`.
This is also available as a coercion `Equiv.coeEmbedding`.
The explicit `Equiv.toEmbedding` version is preferred though, since the coercion can have issues
inferring the type of the resulting embedding. For example:
```lean
-- Works:
example (s : Finset (Fin 3)) (f : Equiv.Perm (Fin 3)) : s.map f.toEmbedding = s.map f := by simp
-- Error, `f` has type `Fin 3 ≃ Fin 3` but is expected to have type `Fin 3 ↪ ?m_1 : Type ?`
example (s : Finset (Fin 3)) (f : Equiv.Perm (Fin 3)) : s.map f = s.map f.toEmbedding := by simp
```
-/
protected def toEmbedding : α ↪ β :=
⟨f, f.injective⟩
