Documentation Verification Report

TimeMan

📁 Source: PhysLean/SpaceAndTime/Time/TimeMan.lean

Statistics

MetricCount
DefinitionsTimeMan, instChartedSpaceReal, instLE, instTopologicalSpace, val, valDiffeomorphism, valHomeomorphism
7
TheoremsinstIsManifoldRealModelWithCornersSelfTopWithTopENat, isOpen_iff, val_contDiff, val_inducing, val_injective, val_isOpenEmbedding, val_range, val_surjective
8
Total15

TimeMan

Definitions

NameCategoryTheorems
instChartedSpaceReal 📖CompOp
2 mathmath: instIsManifoldRealModelWithCornersSelfTopWithTopENat, val_contDiff
instLE 📖CompOp
instTopologicalSpace 📖CompOp
5 mathmath: instIsManifoldRealModelWithCornersSelfTopWithTopENat, val_contDiff, val_isOpenEmbedding, val_inducing, isOpen_iff
val 📖CompOp
7 mathmath: val_contDiff, val_isOpenEmbedding, val_injective, val_inducing, val_range, isOpen_iff, val_surjective
valDiffeomorphism 📖CompOp
valHomeomorphism 📖CompOp

Theorems

NameKindAssumesProvesValidatesDepends On
instIsManifoldRealModelWithCornersSelfTopWithTopENat 📖mathematicalTimeMan
instTopologicalSpace
instChartedSpaceReal
isOpen_iff 📖mathematicalTimeMan
instTopologicalSpace
val
val_isOpenEmbedding
val_contDiff 📖mathematicalTimeMan
instTopologicalSpace
instChartedSpaceReal
val
instIsManifoldRealModelWithCornersSelfTopWithTopENat
val_inducing 📖mathematicalTimeMan
instTopologicalSpace
val
val_injective 📖mathematicalTimeMan
val
val_isOpenEmbedding 📖mathematicalTimeMan
instTopologicalSpace
val
val_injective
val_range
val_range 📖mathematicalTimeMan
val
val_surjective
val_surjective 📖mathematicalTimeMan
val

(root)

Definitions

NameCategoryTheorems
TimeMan 📖CompData
8 mathmath: TimeMan.instIsManifoldRealModelWithCornersSelfTopWithTopENat, TimeMan.val_contDiff, TimeMan.val_isOpenEmbedding, TimeMan.val_injective, TimeMan.val_inducing, TimeMan.val_range, TimeMan.isOpen_iff, TimeMan.val_surjective

---

← Back to Index