OAI/Geometry/IsometricImmersion/Darboux/SixVariableLinearization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.HighEquation.fderiv_axis_eq_deriv_update line 14
  2. def OAI.SmoothLocal.HighEquation.gradientStateIndex line 21
  3. theorem OAI.SmoothLocal.HighEquation.sixVariableP_update_gradient line 23
  4. theorem OAI.SmoothLocal.HighEquation.sixVariableP_update_mixed line 37
  5. theorem OAI.SmoothLocal.HighEquation.sixVariableP_update_yy line 50
  6. theorem OAI.SmoothLocal.HighEquation.solvedDarboux_first_variables_differentiableAt line 63
  7. theorem OAI.SmoothLocal.HighEquation.sixVariableP_gradient_axis line 69
  8. theorem OAI.SmoothLocal.HighEquation.sixVariableP_gradient_axis_at_height line 88
  9. theorem OAI.SmoothLocal.HighEquation.sixVariableP_mixed_axis_at_height line 98
  10. theorem OAI.SmoothLocal.HighEquation.sixVariableP_yy_axis_at_height line 116
  11. theorem OAI.SmoothLocal.HighEquation.sixVariableP_vertical_direction line 137