OAI/Geometry/IsometricImmersion/Darboux/SixVariableDarboux.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.HighEquation.DarbouxState line 13
  2. def OAI.SmoothLocal.HighEquation.statePoint line 15
  3. def OAI.SmoothLocal.HighEquation.stateGradient line 16
  4. def OAI.SmoothLocal.HighEquation.stateBaseDomain line 17
  5. def OAI.SmoothLocal.HighEquation.stateConnection line 19
  6. def OAI.SmoothLocal.HighEquation.stateMixed line 22
  7. def OAI.SmoothLocal.HighEquation.stateDenominator line 25
  8. def OAI.SmoothLocal.HighEquation.stateEnergy line 28
  9. def OAI.SmoothLocal.HighEquation.stateNumerator line 31
  10. def OAI.SmoothLocal.HighEquation.darbouxStateDomain line 34
  11. def OAI.SmoothLocal.HighEquation.sixVariableP line 37
  12. theorem OAI.SmoothLocal.HighEquation.statePoint_contDiff line 40
  13. theorem OAI.SmoothLocal.HighEquation.stateGradient_contDiff line 47
  14. theorem OAI.SmoothLocal.HighEquation.stateBaseDomain_isOpen line 54
  15. theorem OAI.SmoothLocal.HighEquation.stateConnection_contDiffOn line 59
  16. theorem OAI.SmoothLocal.HighEquation.stateMixed_contDiffOn line 67
  17. theorem OAI.SmoothLocal.HighEquation.stateDenominator_contDiffOn line 71
  18. theorem OAI.SmoothLocal.HighEquation.stateEnergy_contDiffOn line 75
  19. theorem OAI.SmoothLocal.HighEquation.stateNumerator_contDiffOn line 87
  20. theorem OAI.SmoothLocal.HighEquation.darbouxStateDomain_isOpen line 93
  21. theorem OAI.SmoothLocal.HighEquation.sixVariableP_contDiffOn line 98
  22. def OAI.SmoothLocal.HighEquation.solutionJet line 105
  23. theorem OAI.SmoothLocal.HighEquation.statePoint_solutionJet line 109
  24. theorem OAI.SmoothLocal.HighEquation.stateGradient_solutionJet line 114
  25. theorem OAI.SmoothLocal.HighEquation.stateDenominator_solutionJet line 119
  26. theorem OAI.SmoothLocal.HighEquation.sixVariableP_solutionJet line 125
  27. theorem OAI.SmoothLocal.HighEquation.solutionJet_contDiffOn line 133
  28. theorem OAI.SmoothLocal.HighEquation.solutionJet_mem_domain line 145