OAI/Geometry/IsometricImmersion/Metrics/MetricPatchOpen.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Perturbation.metricQuadraticValue line 14
  2. theorem OAI.SmoothLocal.Perturbation.metricQuadraticValue_continuousAt line 16
  3. theorem OAI.SmoothLocal.Perturbation.posDef_of_positive_on_sphere line 24
  4. theorem OAI.SmoothLocal.Perturbation.perturbationTensor_isHermitian line 44
  5. theorem OAI.SmoothLocal.Perturbation.perturbedMetric_isHermitian line 51
  6. def OAI.SmoothLocal.Perturbation.metricPositiveSet line 56
  7. theorem OAI.SmoothLocal.Perturbation.metricPositiveSet_mem_nhds line 59
  8. theorem OAI.SmoothLocal.Perturbation.metricPositiveSet_isOpen line 96
  9. theorem OAI.SmoothLocal.Perturbation.centralBox_subset_modelSquare line 101
  10. theorem OAI.SmoothLocal.Perturbation.centralCurvatureJet_eventually line 105
  11. theorem OAI.SmoothLocal.Perturbation.metricPatchSet_isOpen line 124
  12. theorem OAI.SmoothLocal.Perturbation.metricPatchSet_baire line 138
  13. theorem OAI.SmoothLocal.Perturbation.constructedModel_metricPatchSet_isOpen line 144
  14. theorem OAI.SmoothLocal.Perturbation.constructedModel_metricPatchSet_baire line 150