OAI/Geometry/TamingCompatibility/Hodge/HodgeFrameTest.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HodgeChart.coordinateTest line 21
  2. lemma OAI.TamingCompatibility.HodgeChart.coordinateTest_zero line 24
  3. lemma OAI.TamingCompatibility.HodgeChart.coordinateTest_support line 28
  4. lemma OAI.TamingCompatibility.HodgeChart.coordinateTest_smooth line 37
  5. lemma OAI.TamingCompatibility.HodgeChart.coordinateTest_compact line 54
  6. def OAI.TamingCompatibility.HodgeChart.manifoldTest line 58
  7. lemma OAI.TamingCompatibility.HodgeChart.manifoldTest_smooth line 61
  8. lemma OAI.TamingCompatibility.HodgeChart.pullback_manifoldTest line 68
  9. lemma OAI.TamingCompatibility.HodgeChart.manifoldTest_zero_off line 73
  10. def OAI.TamingCompatibility.HodgeChart.rawVector line 79
  11. lemma OAI.TamingCompatibility.HodgeChart.rawVector_smooth line 82
  12. lemma OAI.TamingCompatibility.HodgeChart.rawVector_expansion line 89
  13. lemma OAI.TamingCompatibility.HodgeNormalOperator.vector_fderiv line 104
  14. lemma OAI.TamingCompatibility.HodgeNormalOperator.star_reconstruct_function line 112
  15. lemma OAI.TamingCompatibility.HodgeNormalOperator.reconstruct_function line 118
  16. lemma OAI.TamingCompatibility.HodgeNormalOperator.reconstruct_expansion line 121
  17. def OAI.TamingCompatibility.HodgeChart.normalA line 156
  18. def OAI.TamingCompatibility.HodgeChart.normalB line 158
  19. def OAI.TamingCompatibility.HodgeChart.normalOperator line 161
  20. lemma OAI.TamingCompatibility.HodgeChart.starFrame_smooth line 166
  21. lemma OAI.TamingCompatibility.HodgeChart.normalA_smooth line 176
  22. lemma OAI.TamingCompatibility.HodgeChart.normalB_smooth line 179
  23. lemma OAI.TamingCompatibility.HodgeChart.normal_coordinateTest_at line 188
  24. lemma OAI.TamingCompatibility.HodgeChart.normal_delta line 221
  25. lemma OAI.TamingCompatibility.HodgeChart.normalOperator_zero_off line 245