Injective functions #
Change the value of an embedding
f at one point. If the prescribed image
is already occupied by some
f a', then swap the values at these two points.
f : α ↪ α' is an embedding and
g : Π a, β α ↪ β' (f α) is a family
of embeddings, then
sigma.map f g is an embedding.