Notation

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

Statistics

Metric	Count
Definitions FindModelResult, model, normedSpaceInfo?, NormedSpaceInfo, baseField, normedSpace, findModel, findModelInner, findModels, instCoeExprFindModelResult, instInhabitedFindModelResult, default, instInhabitedNormedSpaceInfo, default, totalSpaceMk, termCMDiffAt____, termCMDiff____, termMDiffAt__, termMDiff__, «termCMDiffAt[_]____», «termCMDiff[_]____», «termHasMFDerivAt%______», «termHasMFDerivAt[_]______», «termMDiffAt[_]__», «termMDiff[_]__», «termMfderiv%__», «termMfderiv[_]__», «termT%_», delabMDifferentiable, delabMDifferentiableAt, delabMDifferentiableOn, delabMDifferentiableWithinAt, delabTotalSpace_mk, delabTotalSpace_mk', delab_mfderiv	35
Theorems	0
Total	35

Manifold

Definitions

Name	Category	Theorems
termCMDiffAt____ 📖	CompOp	—
termCMDiff____ 📖	CompOp	—
termMDiffAt__ 📖	CompOp	—
termMDiff__ 📖	CompOp	—
«termCMDiffAt[_]____» 📖	CompOp	—
«termCMDiff[_]____» 📖	CompOp	—
«termHasMFDerivAt%______» 📖	CompOp	—
«termHasMFDerivAt[_]______» 📖	CompOp	—
«termMDiffAt[_]__» 📖	CompOp	—
«termMDiff[_]__» 📖	CompOp	—
«termMfderiv%__» 📖	CompOp	—
«termMfderiv[_]__» 📖	CompOp	—
«termT%_» 📖	CompOp	—

Manifold.Elab

Definitions

Name	Category	Theorems
FindModelResult 📖	CompData	—
NormedSpaceInfo 📖	CompData	—
findModel 📖	CompOp	—
findModelInner 📖	CompOp	—
findModels 📖	CompOp	—
instCoeExprFindModelResult 📖	CompOp	—
instInhabitedFindModelResult 📖	CompOp	—
instInhabitedNormedSpaceInfo 📖	CompOp	—
totalSpaceMk 📖	CompOp	—

Manifold.Elab.FindModelResult

Definitions

Name	Category	Theorems
model 📖	CompOp	—
normedSpaceInfo? 📖	CompOp	—

Manifold.Elab.NormedSpaceInfo

Definitions

Name	Category	Theorems
baseField 📖	CompOp	—
normedSpace 📖	CompOp	—

Manifold.Elab.instInhabitedFindModelResult

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Manifold.Elab.instInhabitedNormedSpaceInfo

Definitions

Name	Category	Theorems
default 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
delabMDifferentiable 📖	CompOp	—
delabMDifferentiableAt 📖	CompOp	—
delabMDifferentiableOn 📖	CompOp	—
delabMDifferentiableWithinAt 📖	CompOp	—
delabTotalSpace_mk 📖	CompOp	—
delabTotalSpace_mk' 📖	CompOp	—
delab_mfderiv 📖	CompOp	—

---

← Back to Index