OAI/Geometry/IsometricImmersion/Curvature/GaussEquation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.coordPartial_vector_sub line 13
  2. theorem OAI.SmoothLocal.Geometry.coordPartial_vector_sum line 18
  3. theorem OAI.SmoothLocal.Geometry.coordPartial_scalar_vector line 24
  4. theorem OAI.SmoothLocal.Geometry.normalResidual_contDiffOn line 32
  5. theorem OAI.SmoothLocal.Geometry.coordPartial_normalResidual line 41
  6. theorem OAI.SmoothLocal.Geometry.residual_inner_second_eq_residual_inner_residual line 70
  7. theorem OAI.SmoothLocal.Geometry.residual_derivative_inner_tangent line 84
  8. theorem OAI.SmoothLocal.Geometry.second_partial_inner_tangent_eq_christoffel_sum line 110
  9. theorem OAI.SmoothLocal.Geometry.riemann_contraction_eq_residual_products line 123
  10. theorem OAI.SmoothLocal.Geometry.det_secondFundamental_eq_gaussianCurvature_mul_det line 144