# Documentation

Mathlib.Logic.Equiv.Embedding

# Equivalences on embeddings #

This file shows some advanced equivalences on embeddings, useful for constructing larger embeddings from smaller ones.

def Equiv.sumEmbeddingEquivProdEmbeddingDisjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(α β γ) { f // Disjoint (Set.range f.fst) (Set.range f.snd) }

Embeddings from a sum type are equivalent to two separate embeddings with disjoint ranges.

Instances For
def Equiv.codRestrict (α : Type u_1) {β : Type u_2} (bs : Set β) :
{ f // ∀ (a : α), f a bs } (α bs)

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} :
{ f // Disjoint (Set.range f.fst) (Set.range f.snd) } (f : α γ) × (β ())

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
def Equiv.sumEmbeddingEquivSigmaEmbeddingRestricted {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(α β γ) (f : α γ) × (β ())

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.

Instances For
def Equiv.uniqueEmbeddingEquivResult {α : Type u_1} {β : Type u_2} [] :
(α β) β

Embeddings from a single-member type are equivalent to members of the target type.

Instances For