OAI/Geometry/IsometricImmersion/Metrics/PatchTensorRestriction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.assembledPatchTensor line 13
  2. def OAI.SmoothLocal.Geometry.assembledPatchMetric line 16
  3. def OAI.SmoothLocal.Geometry.localPatchMetric line 19
  4. theorem OAI.SmoothLocal.Geometry.assembledPatchTensor_eq_single line 23
  5. theorem OAI.SmoothLocal.Geometry.assembledPatchTensor_zero_off_carriers line 32
  6. theorem OAI.SmoothLocal.Geometry.assembledPatchMetric_pullback_eq_on_closedPatchBox line 41
  7. theorem OAI.SmoothLocal.Geometry.assembledPatchMetric_pullback_eventuallyEq line 56
  8. theorem OAI.SmoothLocal.Geometry.assembledPatchTensor_contDiff line 68
  9. theorem OAI.SmoothLocal.Geometry.assembledPatchTensor_summable line 75
  10. theorem OAI.SmoothLocal.Geometry.assembledPatchTensor_all_jets_zero_at_origin line 81
  11. theorem OAI.SmoothLocal.Geometry.assembledPatchTensor_all_jets_zero_on_disk line 90
  12. theorem OAI.SmoothLocal.Geometry.assembledPatchTensor_jets_eq_single_on_carrier line 101
  13. theorem OAI.SmoothLocal.Geometry.assembledPatchMetric_posDef line 115
  14. theorem OAI.SmoothLocal.Geometry.assembledPatchMetric_smoothPositive line 131
  15. theorem OAI.SmoothLocal.Geometry.assembledPatchMetric_curvature_on_disk line 140