TimeTransMan

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

Statistics

Metric	Count
Definitions `TimeTransMan`, `addTime`, `diff`, `dist`, `instAddActionReal`, `instChartedSpaceReal`, `instLE`, `instTopologicalSpace`, `instVAddReal`, `neg`, `negMetric`, `toTime`, `val`, `valDiffeomorphism`, `valHomeomorphism`	15
Theorems `addTime_eq_val`, `addTime_val`, `diff_eq_toTime_sub`, `diff_eq_val`, `diff_fst_bijective`, `diff_fst_injective`, `diff_fst_surjective`, `diff_self`, `ext_of`, `ext_of_iff`, `instIsManifoldRealModelWithCornersSelfTopWithTopENat`, `instNonempty`, `isOpen_iff`, `le_def`, `neg_eq_negMetric`, `toTime_addTime`, `toTime_neg`, `toTime_symm_add`, `toTime_symm_add'`, `toTime_symm_neg`, `toTime_symm_sub`, `toTime_symm_val`, `toTime_symm_zero_add`, `toTime_val`, `toTime_zero`, `vadd_val`, `val_contDiff`, `val_inducing`, `val_injective`, `val_isOpenEmbedding`, `val_range`, `val_surjective`	32
Total	47

TimeTransMan

Definitions

Name	Category	Theorems
`addTime` 📖	CompOp	7 math math: `addTime_val`, `toTime_symm_add`, `toTime_symm_add'`, `toTime_symm_sub`, `toTime_addTime`, `toTime_symm_val`, `addTime_eq_val`
`diff` 📖	CompOp	10 math math: `toTime_symm_add`, `toTime_val`, `toTime_symm_add'`, `diff_fst_bijective`, `toTime_symm_sub`, `diff_eq_toTime_sub`, `diff_fst_injective`, `diff_fst_surjective`, `diff_self`, `diff_eq_val`
`dist` 📖	CompOp	—
`instAddActionReal` 📖	CompOp	—
`instChartedSpaceReal` 📖	CompOp	2 math math: `val_contDiff`, `instIsManifoldRealModelWithCornersSelfTopWithTopENat`
`instLE` 📖	CompOp	1 math math: `le_def`
`instTopologicalSpace` 📖	CompOp	16 math math: `val_isOpenEmbedding`, `toTime_symm_add`, `val_contDiff`, `toTime_val`, `toTime_symm_add'`, `toTime_symm_sub`, `diff_eq_toTime_sub`, `toTime_addTime`, `toTime_symm_neg`, `toTime_symm_val`, `isOpen_iff`, `instIsManifoldRealModelWithCornersSelfTopWithTopENat`, `val_inducing`, `toTime_neg`, `toTime_zero`, `toTime_symm_zero_add`
`instVAddReal` 📖	CompOp	1 math math: `vadd_val`
`neg` 📖	CompOp	3 math math: `neg_eq_negMetric`, `toTime_symm_neg`, `toTime_neg`
`negMetric` 📖	CompOp	1 math math: `neg_eq_negMetric`
`toTime` 📖	CompOp	11 math math: `toTime_symm_add`, `toTime_val`, `toTime_symm_add'`, `toTime_symm_sub`, `diff_eq_toTime_sub`, `toTime_addTime`, `toTime_symm_neg`, `toTime_symm_val`, `toTime_neg`, `toTime_zero`, `toTime_symm_zero_add`
`val` 📖	CompOp	13 math math: `val_isOpenEmbedding`, `addTime_val`, `val_contDiff`, `val_range`, `le_def`, `val_injective`, `isOpen_iff`, `diff_eq_val`, `val_surjective`, `addTime_eq_val`, `vadd_val`, `ext_of_iff`, `val_inducing`
`valDiffeomorphism` 📖	CompOp	—
`valHomeomorphism` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addTime_eq_val` 📖	mathematical	—	`addTime` `TimeUnit.val` `val`	—	`diff_fst_injective` `instNonempty` `diff_fst_surjective` `diff_eq_val`
`addTime_val` 📖	mathematical	—	`val` `addTime` `TimeUnit.val`	—	`addTime_eq_val`
`diff_eq_toTime_sub` 📖	mathematical	—	`diff` `Time.val` `TimeTransMan` `Time` `instTopologicalSpace` `Time.instSeminormedAddCommGroup` `toTime`	—	`diff_eq_val` `toTime_val`
`diff_eq_val` 📖	mathematical	—	`diff` `TimeUnit.val` `val`	—	`TimeUnit.val_neq_zero`
`diff_fst_bijective` 📖	mathematical	—	`TimeTransMan` `diff`	—	`diff_fst_injective` `diff_fst_surjective`
`diff_fst_injective` 📖	mathematical	—	`TimeTransMan` `diff`	—	`ext_of`
`diff_fst_surjective` 📖	mathematical	—	`TimeTransMan` `diff`	—	`TimeUnit.val_pos`
`diff_self` 📖	mathematical	—	`diff`	—	`diff_eq_val`
`ext_of` 📖	—	`val`	—	—	—
`ext_of_iff` 📖	mathematical	—	`val`	—	`ext_of`
`instIsManifoldRealModelWithCornersSelfTopWithTopENat` 📖	mathematical	—	`TimeTransMan` `instTopologicalSpace` `instChartedSpaceReal`	—	—
`instNonempty` 📖	mathematical	—	`TimeTransMan`	—	—
`isOpen_iff` 📖	mathematical	—	`TimeTransMan` `instTopologicalSpace` `val`	—	`val_isOpenEmbedding`
`le_def` 📖	mathematical	—	`TimeTransMan` `instLE` `val`	—	—
`neg_eq_negMetric` 📖	mathematical	—	`neg` `negMetric`	—	`ext_of` `diff_eq_val` `addTime_val`
`toTime_addTime` 📖	mathematical	—	`TimeTransMan` `Time` `instTopologicalSpace` `Time.instSeminormedAddCommGroup` `toTime` `addTime` `Time.instAdd`	—	`Time.ext` `toTime_val` `diff_eq_val` `addTime_val`
`toTime_neg` 📖	mathematical	—	`TimeTransMan` `Time` `instTopologicalSpace` `Time.instSeminormedAddCommGroup` `toTime` `neg` `Time.instNeg`	—	`neg_eq_negMetric` `Time.ext` `diff_eq_val` `toTime_addTime` `toTime_zero` `toTime_val`
`toTime_symm_add` 📖	mathematical	—	`Time` `TimeTransMan` `Time.instSeminormedAddCommGroup` `instTopologicalSpace` `toTime` `Time.instAdd` `addTime` `diff`	—	`ext_of` `toTime_symm_val` `addTime_val` `diff_eq_val`
`toTime_symm_add'` 📖	mathematical	—	`Time` `TimeTransMan` `Time.instSeminormedAddCommGroup` `instTopologicalSpace` `toTime` `Time.instAdd` `addTime` `diff`	—	`ext_of` `toTime_symm_val` `addTime_val` `diff_eq_val`
`toTime_symm_neg` 📖	mathematical	—	`Time` `TimeTransMan` `Time.instSeminormedAddCommGroup` `instTopologicalSpace` `toTime` `Time.instNeg` `neg`	—	`ext_of` `toTime_symm_val` `addTime_val` `diff_eq_val`
`toTime_symm_sub` 📖	mathematical	—	`Time` `TimeTransMan` `Time.instSeminormedAddCommGroup` `instTopologicalSpace` `toTime` `Time.instSub` `addTime` `diff`	—	`ext_of` `toTime_symm_val` `addTime_val` `diff_eq_val`
`toTime_symm_val` 📖	mathematical	—	`Time` `TimeTransMan` `Time.instSeminormedAddCommGroup` `instTopologicalSpace` `toTime` `addTime` `Time.val`	—	`ext_of` `diff_eq_val` `addTime_val`
`toTime_symm_zero_add` 📖	mathematical	—	`Time` `TimeTransMan` `Time.instSeminormedAddCommGroup` `instTopologicalSpace` `toTime` `Time.instOfNat`	—	`ext_of` `diff_eq_val` `Time.zero_val` `addTime_val`
`toTime_val` 📖	mathematical	—	`Time.val` `TimeTransMan` `Time` `instTopologicalSpace` `Time.instSeminormedAddCommGroup` `toTime` `diff`	—	—
`toTime_zero` 📖	mathematical	—	`TimeTransMan` `Time` `instTopologicalSpace` `Time.instSeminormedAddCommGroup` `toTime` `Time.instOfNat`	—	`Time.ext` `diff_eq_val` `Time.zero_val`
`vadd_val` 📖	mathematical	—	`val` `TimeTransMan` `instVAddReal`	—	—
`val_contDiff` 📖	mathematical	—	`TimeTransMan` `instTopologicalSpace` `instChartedSpaceReal` `val`	—	`instIsManifoldRealModelWithCornersSelfTopWithTopENat`
`val_inducing` 📖	mathematical	—	`TimeTransMan` `instTopologicalSpace` `val`	—	—
`val_injective` 📖	mathematical	—	`TimeTransMan` `val`	—	—
`val_isOpenEmbedding` 📖	mathematical	—	`TimeTransMan` `instTopologicalSpace` `val`	—	`val_injective` `val_range`
`val_range` 📖	mathematical	—	`TimeTransMan` `val`	—	`val_surjective`
`val_surjective` 📖	mathematical	—	`TimeTransMan` `val`	—	—

(root)

Definitions

Name	Category	Theorems
`TimeTransMan` 📖	CompData	25 math math: `TimeTransMan.val_isOpenEmbedding`, `TimeTransMan.toTime_symm_add`, `TimeTransMan.val_contDiff`, `TimeTransMan.toTime_val`, `TimeTransMan.toTime_symm_add'`, `TimeTransMan.diff_fst_bijective`, `TimeTransMan.toTime_symm_sub`, `TimeTransMan.diff_eq_toTime_sub`, `TimeTransMan.toTime_addTime`, `TimeTransMan.toTime_symm_neg`, `TimeTransMan.diff_fst_injective`, `TimeTransMan.diff_fst_surjective`, `TimeTransMan.val_range`, `TimeTransMan.le_def`, `TimeTransMan.toTime_symm_val`, `TimeTransMan.val_injective`, `TimeTransMan.isOpen_iff`, `TimeTransMan.val_surjective`, `TimeTransMan.vadd_val`, `TimeTransMan.instIsManifoldRealModelWithCornersSelfTopWithTopENat`, `TimeTransMan.val_inducing`, `TimeTransMan.instNonempty`, `TimeTransMan.toTime_neg`, `TimeTransMan.toTime_zero`, `TimeTransMan.toTime_symm_zero_add`

---

← Back to Index