function.embedding.some

Embedding into option

function.embedding.cod_restrict

Restrict the codomain of an embedding.

set.embedding_of_subset

The injection map is an embedding between subsets.