OAI/Geometry/IsometricImmersion/Metrics/MetricLocality.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.coordPartial_eq_of_eventuallyEq line 15
  2. theorem OAI.SmoothLocal.Geometry.coordPartial_eventuallyEq line 22
  3. def OAI.SmoothLocal.Geometry.iteratedCoordPartial line 29
  4. theorem OAI.SmoothLocal.Geometry.iteratedCoordPartial_eventuallyEq line 34
  5. theorem OAI.SmoothLocal.Geometry.iteratedCoordPartial_zero line 42
  6. theorem OAI.SmoothLocal.Geometry.eventuallyEq_zero_of_not_mem_tsupport line 54
  7. theorem OAI.SmoothLocal.Geometry.iteratedCoordPartial_zero_of_not_mem_tsupport line 62
  8. theorem OAI.SmoothLocal.Geometry.metric_coeff_eventuallyEq line 71
  9. theorem OAI.SmoothLocal.Geometry.christoffel_eq_of_eventuallyEq line 76
  10. theorem OAI.SmoothLocal.Geometry.christoffel_eventuallyEq line 85
  11. theorem OAI.SmoothLocal.Geometry.riemann_eq_of_eventuallyEq line 90
  12. theorem OAI.SmoothLocal.Geometry.gaussianCurvature_eq_of_eventuallyEq line 99
  13. theorem OAI.SmoothLocal.Geometry.covHessian_eq_of_metric_eventuallyEq line 103
  14. theorem OAI.SmoothLocal.Geometry.heightEnergy_eq_of_metric_eventuallyEq line 108
  15. theorem OAI.SmoothLocal.Geometry.metric_add_eventuallyEq_of_not_mem_tsupport line 112
  16. theorem OAI.SmoothLocal.Geometry.metric_add_all_coordinate_jets line 118
  17. theorem OAI.SmoothLocal.Geometry.gaussianCurvature_add_eq_off_tsupport line 124