Documentation Verification Report

TimeMan

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

Statistics

Metric	Count
Definitions `TimeMan`, `instChartedSpaceReal`, `instLE`, `instTopologicalSpace`, `val`, `valDiffeomorphism`, `valHomeomorphism`	7
Theorems `instIsManifoldRealModelWithCornersSelfTopWithTopENat`, `isOpen_iff`, `val_contDiff`, `val_inducing`, `val_injective`, `val_isOpenEmbedding`, `val_range`, `val_surjective`	8
Total	15

TimeMan

Definitions

Name	Category	Theorems
`instChartedSpaceReal` 📖	CompOp	2 math math: `instIsManifoldRealModelWithCornersSelfTopWithTopENat`, `val_contDiff`
`instLE` 📖	CompOp	—
`instTopologicalSpace` 📖	CompOp	5 math math: `instIsManifoldRealModelWithCornersSelfTopWithTopENat`, `val_contDiff`, `val_isOpenEmbedding`, `val_inducing`, `isOpen_iff`
`val` 📖	CompOp	7 math math: `val_contDiff`, `val_isOpenEmbedding`, `val_injective`, `val_inducing`, `val_range`, `isOpen_iff`, `val_surjective`
`valDiffeomorphism` 📖	CompOp	—
`valHomeomorphism` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsManifoldRealModelWithCornersSelfTopWithTopENat` 📖	mathematical	—	`TimeMan` `instTopologicalSpace` `instChartedSpaceReal`	—	—
`isOpen_iff` 📖	mathematical	—	`TimeMan` `instTopologicalSpace` `val`	—	`val_isOpenEmbedding`
`val_contDiff` 📖	mathematical	—	`TimeMan` `instTopologicalSpace` `instChartedSpaceReal` `val`	—	`instIsManifoldRealModelWithCornersSelfTopWithTopENat`
`val_inducing` 📖	mathematical	—	`TimeMan` `instTopologicalSpace` `val`	—	—
`val_injective` 📖	mathematical	—	`TimeMan` `val`	—	—
`val_isOpenEmbedding` 📖	mathematical	—	`TimeMan` `instTopologicalSpace` `val`	—	`val_injective` `val_range`
`val_range` 📖	mathematical	—	`TimeMan` `val`	—	`val_surjective`
`val_surjective` 📖	mathematical	—	`TimeMan` `val`	—	—

(root)

Definitions

Name	Category	Theorems
`TimeMan` 📖	CompData	8 math math: `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