Equivalences on embeddings #
This file shows some advanced equivalences on embeddings, useful for constructing larger embeddings from smaller ones.
Embeddings whose range lies within a set are equivalent to embeddings to that set.
This is Function.Embedding.codRestrict
as an equiv.
Instances For
def
Equiv.prodEmbeddingDisjointEquivSigmaEmbeddingRestricted
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
:
Pairs of embeddings with disjoint ranges are equivalent to a dependent sum of embeddings, in which the second embedding cannot take values in the range of the first.
Instances For
A combination of the above results, allowing us to turn one embedding over a sum type into two dependent embeddings, the second of which avoids any members of the range of the first. This is helpful for constructing larger embeddings out of smaller ones.