OAI/Geometry/NodalSets/Charts/FrameMapFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Geometry.frameMap line 11
  2. lemma OAI.Yau.Geometry.frameMap_apply line 14
  3. lemma OAI.Yau.Geometry.frameMap_axis line 17
  4. lemma OAI.Yau.Geometry.frameMap_pair line 20
  5. lemma OAI.Yau.Geometry.frameMap_injective line 25
  6. def OAI.Yau.Geometry.frameEquiv line 31
  7. lemma OAI.Yau.Geometry.frameEquiv_coe line 35
  8. lemma OAI.Yau.Geometry.frameMap_continuous line 40
  9. theorem OAI.Yau.Geometry.frameEquiv_continuous line 46
  10. lemma OAI.Yau.Geometry.frameConnection_continuous line 52
  11. theorem OAI.Yau.Geometry.quadratic_chart_maps_joint_continuous line 58