OAI/Geometry/NodalSets/Charts/MetricFrameOps.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Geometry.metricNormalize line 11
  2. lemma OAI.Yau.Geometry.metricNormalize_unit line 14
  3. lemma OAI.Yau.Geometry.metricNormalize_fixed line 22
  4. lemma OAI.Yau.Geometry.metricNormalize_orthogonal line 25
  5. def OAI.Yau.Geometry.removeFrame line 29
  6. lemma OAI.Yau.Geometry.removeFrame_orthogonal line 32
  7. lemma OAI.Yau.Geometry.removeFrame_fixed line 38
  8. lemma OAI.Yau.Geometry.metricNormalize_continuousAt line 42
  9. lemma OAI.Yau.Geometry.metricNormalize_continuous line 48
  10. lemma OAI.Yau.Geometry.removeFrame_continuousAt line 53
  11. lemma OAI.Yau.Geometry.removeFrame_continuous line 66