Embedding

📁 Source: Mathlib/Data/FunLike/Embedding.lean

Statistics

Metric	Count
Definitions EmbeddingLike	1
Theorems apply_eq_iff_eq, comp_injective, injective, injective'	4
Total	5

EmbeddingLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_iff_eq 📖	mathematical	—	DFunLike.coe	—	injective
comp_injective 📖	mathematical	—	DFunLike.coe	—	Function.Injective.of_comp_iff injective
injective 📖	mathematical	—	DFunLike.coe	—	injective'
injective' 📖	mathematical	—	DFunLike.coe	—	—

(root)

Definitions

Name	Category	Theorems
EmbeddingLike 📖	CompData	6 math math: Function.instEmbeddingLikeEmbedding, RelEmbedding.instEmbeddingLike, EquivLike.toEmbeddingLike, FirstOrder.Language.Embedding.embeddingLike, FirstOrder.Language.ElementaryEmbedding.embeddingLike, InitialSeg.instEmbeddingLike

---

← Back to Index