OAI/Geometry/IsometricImmersion/Darboux/MixedDarbouxElimination.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.mixedFaaTerm line 13
  2. def OAI.SmoothLocal.HighEquation.mixedFaaFactor line 18
  3. def OAI.SmoothLocal.HighEquation.mixedFaaRemainder line 22
  4. def OAI.SmoothLocal.HighEquation.mixedBlockWord line 28
  5. def OAI.SmoothLocal.HighEquation.heightStateSuffix line 31
  6. theorem OAI.SmoothLocal.HighEquation.heightStateSuffix_length line 33
  7. theorem OAI.SmoothLocal.HighEquation.heightStateFactor_zero_eq_suffix line 37
  8. theorem OAI.SmoothLocal.HighEquation.mixedFaaTerm_scalar_expansion line 41
  9. theorem OAI.SmoothLocal.HighEquation.mixedFaaFactor_height_slot line 49
  10. theorem OAI.SmoothLocal.HighEquation.mixed_coordinate_height_factor_eq_word line 59
  11. theorem OAI.SmoothLocal.HighEquation.mixedFaaFactor_spatial_slot line 77
  12. theorem OAI.SmoothLocal.HighEquation.mixed_nonfull_factor_order line 88
  13. theorem OAI.SmoothLocal.HighEquation.mixed_nonfull_height_word_length line 96
  14. theorem OAI.SmoothLocal.HighEquation.mixedFaaRemainder_coordinate_eq line 105
  15. theorem OAI.SmoothLocal.HighEquation.actualP_mixed_faaExpansion line 120
  16. theorem OAI.SmoothLocal.HighEquation.mixed_fullBlock_term line 135
  17. theorem OAI.SmoothLocal.HighEquation.mixed_fullBlock_linearization line 145
  18. theorem OAI.SmoothLocal.HighEquation.actualDarboux_mixed_principal line 161
  19. theorem OAI.SmoothLocal.HighEquation.actualDarboux_ordered_mixed_elimination line 189
  20. theorem OAI.SmoothLocal.HighEquation.actualDarboux_arbitrary_word_elimination line 211