OAI/Geometry/TamingCompatibility/Functional/ChartNormalTest.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TamingCompatibility.LocalMatrixOperator.pair_fderiv line 15
  2. def OAI.TamingCompatibility.GeometricChart.normalA line 34
  3. def OAI.TamingCompatibility.GeometricChart.normalB line 37
  4. lemma OAI.TamingCompatibility.GeometricChart.normal_coordinateTest line 45
  5. lemma OAI.TamingCompatibility.GeometricChart.normal_manifoldTest_delta line 76
  6. def OAI.TamingCompatibility.LocalMatrixOperator.normalizeFrame line 103
  7. lemma OAI.TamingCompatibility.LocalMatrixOperator.normalizeFrame_apply line 108
  8. lemma OAI.TamingCompatibility.LocalMatrixOperator.normalized_frameCovector line 116
  9. lemma OAI.TamingCompatibility.GeometricChart.normalA_smooth line 130
  10. lemma OAI.TamingCompatibility.GeometricChart.realDeriv_smooth line 144
  11. lemma OAI.TamingCompatibility.GeometricChart.imagDeriv_smooth line 151
  12. lemma OAI.TamingCompatibility.GeometricChart.normalStar_smooth line 158
  13. lemma OAI.TamingCompatibility.GeometricChart.normalB_smooth line 170
  14. def OAI.TamingCompatibility.GeometricChart.normalMetric line 187
  15. lemma OAI.TamingCompatibility.GeometricChart.normalMetric_smooth line 190