Injective functions #
- toFun : α → β
An embedding as a function. Use coercion instead.
- inj' : Function.Injective s.toFun
An embedding is an injective function. Use
Function.Embedding.injective
instead.
α ↪ β
is a bundled injective function.
Instances For
An embedding, a.k.a. a bundled injective function.
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
Instances For
The identity map as a Function.Embedding
.
Instances For
A right inverse surjInv
of a surjective function as an Embedding
.
Instances For
Convert a surjective Embedding
to an Equiv
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.
Instances For
A version of Option.map
for Function.Embedding
s.
Instances For
Quotient.out
as an embedding.
Instances For
Choosing an element b : β
gives an embedding of PUnit
into β
.
Instances For
Sigma.mk
as a Function.Embedding
.
Instances For
If f : α ↪ α'
is an embedding and g : Π a, β α ↪ β' (f α)
is a family
of embeddings, then Sigma.map f g
is an embedding.
Instances For
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)
.
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
.
Instances For
The type of embeddings α ↪ β
is equivalent to
the subtype of all injective functions α → β
.
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.