Theorems · Definition · logic and foundations

Equiv.toEmbedding

{α : Sort u} → {β : Sort v} → α ≃ β → α ↪ β

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 ``

Defined in

Mathlib.Logic.Embedding.Basic

Cited by

254 results in Mathlib

Foundations

Depth 15 from the axioms, rests on 60 definitions · uses Quot.sound