OAI/Geometry/TamingCompatibility/DifferentialForms/FirstMatrixJoint.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.firstMatrix_joint line 19
2. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.zeroMatrix_joint line 36
3. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.gaugeFirst_joint line 61
4. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.gaugeZero_joint line 72
5. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.gauge_joint line 88
6. def OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.regularMetrics line 108
7. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.regularMetrics_open line 111
8. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.euclidean_mem_regularMetrics line 115
9. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.volumeDensity_contDiffAt_regular line 121
10. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.volumeDensity_pos line 125
11. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.principal_contDiffAt_regular line 128
12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ActualData.jets line 144