Structures · Data types
EmbeddingLike
The class EmbeddingLike F α β expresses that terms of type F have an
injective coercion to injective functions α ↪ β.
- Defined in
- Mathlib.Data.FunLike.Embedding
- Shape
- 3 explicit arguments · adds injective'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- Function.Embedding
- RelEmbedding
- InitialSeg
- FirstOrder.Language.Embedding
- FirstOrder.Language.ElementaryEmbedding
How is a type an instance?
Loading the hierarchy index…
Assumed by21
- EmbeddingLike.apply_eq_iff_eq
- EmbeddingLike.injective
- EmbeddingLike.map_eq_zero_iff
- EmbeddingLike.map_ne_zero_iff
- FirstOrder.Language.StrongHomClass.toEmbedding
- EmbeddingLike.map_eq_one_iff
- EmbeddingLike.comp_injective
- EmbeddingLike.map_ne_one_iff
- FirstOrder.Language.BoundedFormula.IsQF.realize_embedding
- FirstOrder.Language.HomClass.strictMono
- FirstOrder.Language.BoundedFormula.IsUniversal.realize_embedding
- EmbeddingLike.injective'
- Fintype.card_range
- EmbeddingLike.pairwise_comp
- MulEquivClass.map_ne_one_iff
- AddEquivClass.map_ne_zero_iff
- MulEquivClass.map_eq_one_iff
- FirstOrder.Language.StrongHomClass.toEmbedding_toFun
- AddEquivClass.map_eq_zero_iff
- FirstOrder.Language.BoundedFormula.IsExistential.realize_embedding
- FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp
Ancestors0
No ancestors.