mathlib3 documentation


Equivalences on embeddings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def equiv.sum_embedding_equiv_prod_embedding_disjoint {α : 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.

def equiv.cod_restrict (α : 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.cod_restrict as an equiv.


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.

def equiv.sum_embedding_equiv_sigma_embedding_restricted {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
β γ) Σ (f : α γ), β (set.range 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.

def equiv.unique_embedding_equiv_result {α : Type u_1} {β : Type u_2} [unique α] :
β) β

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