OAI/Geometry/TamingCompatibility/Charts/MetricCalculus.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.V line 17
2. abbrev OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.EMetric line 21
3. def OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.volumeDensity line 23
4. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.gram_euclidean line 26
5. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.volumeDensity_euclidean line 30
6. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.detGram_contDiff line 33
7. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.volumeDensity_contDiffAt line 39
8. def OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.metricOperator line 43
9. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.metricOperator_apply line 47
10. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.metricOperator_euclidean line 50
11. def OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.cometric line 55
12. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.cometric_euclidean line 58
13. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.cometric_contDiffAt line 62
14. def OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.principal line 67
15. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.principal_euclidean line 71
16. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.principal_contDiffAt line 74
17. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.jets line 78