OAI/Geometry/IsometricImmersion/Darboux/SixVariableQ.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.qToPStateIndex line 13
  2. def OAI.SmoothLocal.HighEquation.qToPState line 15
  3. def OAI.SmoothLocal.HighEquation.qToPStateLinear line 17
  4. def OAI.SmoothLocal.HighEquation.qToPStateCLM line 22
  5. theorem OAI.SmoothLocal.HighEquation.qToPStateCLM_apply line 25
  6. theorem OAI.SmoothLocal.HighEquation.qToPStateIndex_involutive line 27
  7. theorem OAI.SmoothLocal.HighEquation.qToPState_involutive line 31
  8. theorem OAI.SmoothLocal.HighEquation.qToPState_contDiff line 35
  9. theorem OAI.SmoothLocal.HighEquation.qToPState_hasFDerivAt line 37
  10. theorem OAI.SmoothLocal.HighEquation.qToPState_single line 40
  11. theorem OAI.SmoothLocal.HighEquation.statePoint_qToPState line 46
  12. theorem OAI.SmoothLocal.HighEquation.stateGradient_qToPState line 51
  13. theorem OAI.SmoothLocal.HighEquation.qToPState_four line 56
  14. theorem OAI.SmoothLocal.HighEquation.qToPState_five line 57
  15. def OAI.SmoothLocal.HighEquation.stateQDenominator line 59
  16. def OAI.SmoothLocal.HighEquation.darbouxQStateDomain line 62
  17. def OAI.SmoothLocal.HighEquation.sixVariableQ line 65
  18. theorem OAI.SmoothLocal.HighEquation.stateDenominator_qToPState line 68
  19. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_explicit line 78
  20. theorem OAI.SmoothLocal.HighEquation.darbouxQStateDomain_eq_preimage line 88
  21. theorem OAI.SmoothLocal.HighEquation.qToPState_mem_domain line 103
  22. theorem OAI.SmoothLocal.HighEquation.darbouxQStateDomain_isOpen line 109
  23. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_contDiffOn line 115
  24. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_axis_eq_swappedP line 122
  25. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_spatial_x line 137
  26. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_spatial_y line 144
  27. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_update_gradient line 151
  28. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_update_mixed line 167
  29. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_update_xx line 181
  30. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_gradient_axis line 195
  31. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_gradient_axis_expanded line 215
  32. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_mixed_axis line 228
  33. theorem OAI.SmoothLocal.HighEquation.sixVariableQ_xx_axis line 242
  34. def OAI.SmoothLocal.HighEquation.qSolutionJet line 257
  35. theorem OAI.SmoothLocal.HighEquation.statePoint_qSolutionJet line 261
  36. theorem OAI.SmoothLocal.HighEquation.stateGradient_qSolutionJet line 266
  37. theorem OAI.SmoothLocal.HighEquation.stateQDenominator_qSolutionJet line 271
  38. theorem OAI.SmoothLocal.HighEquation.qToPState_qSolutionJet line 277
  39. theorem OAI.SmoothLocal.HighEquation.qSolutionJet_mem_domain line 295
  40. theorem OAI.SmoothLocal.HighEquation.darbouxDet_iff_sixVariableQ line 302