Injective functions #
α ↪ β
is a bundled injective function.
- toFun : α → β
An embedding as a function. Use coercion instead.
An embedding is an injective function. Use
Function.Embedding.injective
instead.
Instances For
An embedding, a.k.a. a bundled injective function.
Equations
Instances For
Convert an α ≃ β
to α ↪ β
.
This is also available as a coercion Equiv.coeEmbedding
.
The explicit Equiv.toEmbedding
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.toEmbedding = 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.toEmbedding := by simp
Equations
Instances For
A right inverse surjInv
of a surjective function as an Embedding
.
Equations
Instances For
Convert a surjective Embedding
to an Equiv
Equations
Instances For
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.
Equations
Instances For
Alias of Function.Embedding.sectL
.
Fixing an element b : β
gives an embedding α ↪ α × β
.
Equations
Instances For
Alias of Function.Embedding.sectR
.
Fixing an element a : α
gives an embedding β ↪ α × β
.
Equations
Instances For
Alias of Function.Embedding.sectL_apply
.
Alias of Function.Embedding.sectR_apply
.
Define an embedding (Π a : α, β a) ↪ (Π a : α, γ a)
from a family of embeddings
e : Π a, (β a ↪ γ a)
. This embedding sends f
to fun a ↦ e a (f a)
.
Equations
Instances For
An embedding e : α ↪ β
defines an embedding (α → γ) ↪ (β → γ)
for any inhabited type γ
.
This embedding sends each f : α → γ
to a function g : β → γ
such that g ∘ e = f
and
g y = default
whenever y ∉ range e
.
Equations
Instances For
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.