Convert an α ≃ β to α ↪ β.

This is also available as a coercion equiv.coe_embedding. The explicit equiv.to_embedding version is preferred though, since the coercion can have issues inferring the type of the resulting embedding. For example:

-- Works:
example (s : finset (fin 3)) (f : equiv.perm (fin 3)) : s.map f.to_embedding = s.map f := by simp
-- Error, `f` has type `fin 3 ≃ fin 3` but is expected to have type `fin 3 ↪ ?m_1 : Type ?`
example (s : finset (fin 3)) (f : equiv.perm (fin 3)) : s.map f = s.map f.to_embedding := by simp

Given an equivalence to a subtype, produce an embedding to the elements of the corresponding set.

The identity map as a function.embedding.

Composition of f : α ↪ β and g : β ↪ γ.

Transfer an embedding along a pair of equivalences.

There is always an embedding from an empty type. -

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.

Embedding into option α using some.

Embedding into option α using coe. Usually the correct synctatical form for simp.

Embedding into with_top α.

Given an embedding f : α ↪ β and a point outside of set.range f, construct an embedding option α ↪ β.

Equivalence between embeddings of option α and a sigma type over the embeddings of α.

A version of option.map for function.embeddings.

Embedding of a subtype.

Choosing an element b : β gives an embedding of punit into β.

Fixing an element b : β gives an embedding α ↪ α × β.

Fixing an element a : α gives an embedding β ↪ α × β.

Restrict the codomain of an embedding.

If e₁ and e₂ are embeddings, then so is prod.map e₁ e₂ : (a, b) ↦ (e₁ a, e₂ b).

If e₁ and e₂ are embeddings, then so is λ ⟨a, b⟩, ⟨e₁ a, e₂ b⟩ : pprod α γ → pprod β δ.

If e₁ and e₂ are embeddings, then so is sum.map e₁ e₂.

The embedding of α into the sum α ⊕ β.

The embedding of β into the sum α ⊕ β.

sigma.mk as an function.embedding.

If f : α ↪ α' is an embedding and g : Π a, β α ↪ β' (f α) is a family of embeddings, then sigma.map f g is an embedding.

Define an embedding (Π a : α, β a) ↪ (Π a : α, γ a) from a family of embeddings e : Π a, (β a ↪ γ a). This embedding sends f to λ a, e a (f a).

An embedding e : α ↪ β defines an embedding (γ → α) ↪ (γ → β) that sends each f to e ∘ f.

Restrict both domain and codomain of an embedding.

set.image as an embedding set α ↪ set β.

The type of embeddings α ↪ β is equivalent to the subtype of all injective functions α → β.

If α₁ ≃ α₂ and β₁ ≃ β₂, then the type of embeddings α₁ ↪ β₁ is equivalent to the type of embeddings α₂ ↪ β₂.

The injection map is an embedding between subsets.

A subtype {x // p x ∨ q x} over a disjunction of p q : α → Prop can be injectively split into a sum of subtypes {x // p x} ⊕ {x // q x} such that ¬ p x is sent to the right.

A subtype {x // p x} can be injectively sent to into a subtype {x // q x}, if p x → q x for all x : α.

A subtype {x // p x ∨ q x} over a disjunction of p q : α → Prop is equivalent to a sum of subtypes {x // p x} ⊕ {x // q x} such that ¬ p x is sent to the right, when disjoint p q.

See also equiv.sum_compl, for when is_compl p q.