SmoothEmbedding

📁 Source: Mathlib/Geometry/Manifold/SmoothEmbedding.lean

Statistics

Metric	Count
Definitions IsSmoothEmbedding	1
Theorems id, isEmbedding, isImmersion, of_opens, prodMap, isSmoothEmbedding_iff	6
Total	7

Manifold

Definitions

Name	Category	Theorems
IsSmoothEmbedding 📖	CompData	3 math math: IsSmoothEmbedding.id, isSmoothEmbedding_iff, IsSmoothEmbedding.of_opens

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSmoothEmbedding_iff 📖	mathematical	—	IsSmoothEmbedding IsImmersion Topology.IsEmbedding	—	—

Manifold.IsSmoothEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
id 📖	mathematical	—	Manifold.IsSmoothEmbedding	—	Manifold.IsImmersion.id Topology.IsEmbedding.id
isEmbedding 📖	mathematical	Manifold.IsSmoothEmbedding	Topology.IsEmbedding	—	—
isImmersion 📖	mathematical	Manifold.IsSmoothEmbedding	Manifold.IsImmersion	—	—
of_opens 📖	mathematical	—	Manifold.IsSmoothEmbedding TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace	—	Manifold.isSmoothEmbedding_iff Manifold.IsImmersion.of_opens Topology.IsEmbedding.subtypeVal
prodMap 📖	mathematical	Manifold.IsSmoothEmbedding	Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod instTopologicalSpaceProd prodChartedSpace	—	Manifold.IsImmersion.prodMap isImmersion Topology.IsEmbedding.prodMap isEmbedding

---

← Back to Index