OAI/Geometry/IsometricImmersion/Assembly/SupportedMetricJets.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Perturbation.metricCoefficientCLM line 13
  2. theorem OAI.SmoothLocal.Perturbation.supportedTensor_coeff_iteratedFDeriv line 19
  3. theorem OAI.SmoothLocal.Perturbation.supportedTensor_coordPartial_eq_jet line 28
  4. theorem OAI.SmoothLocal.Perturbation.supportedTensor_second_coordPartial_eq_jet line 35
  5. theorem OAI.SmoothLocal.Perturbation.supportedTensor_coeff_eval_joint_continuous line 45
  6. theorem OAI.SmoothLocal.Perturbation.supportedTensor_coordPartial_joint_continuous line 49
  7. theorem OAI.SmoothLocal.Perturbation.supportedTensor_second_coordPartial_joint_continuous line 58
  8. theorem OAI.SmoothLocal.Perturbation.perturbationTensor_coeff_eval_joint_continuous line 67
  9. theorem OAI.SmoothLocal.Perturbation.perturbationTensor_coordPartial_joint_continuous line 72
  10. theorem OAI.SmoothLocal.Perturbation.perturbationTensor_second_coordPartial_joint_continuous line 78
  11. theorem OAI.SmoothLocal.Perturbation.perturbedMetric_coordPartial line 84
  12. theorem OAI.SmoothLocal.Perturbation.perturbedMetric_second_coordPartial line 94
  13. theorem OAI.SmoothLocal.Perturbation.perturbedMetric_coeff_joint_continuousAt line 119
  14. theorem OAI.SmoothLocal.Perturbation.perturbedMetric_coordPartial_joint_continuousAt line 126
  15. theorem OAI.SmoothLocal.Perturbation.perturbedMetric_second_coordPartial_joint_continuousAt line 137
  16. def OAI.SmoothLocal.Perturbation.perturbedCurvatureJet line 150
  17. theorem OAI.SmoothLocal.Perturbation.perturbedCurvatureJet_joint_continuousAt line 155
  18. theorem OAI.SmoothLocal.Perturbation.gaussianCurvature_perturbedMetric_eq_jet line 164