OAI/Analysis/SymmetricDomains/OldOffsetOldPosition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.analytic_chart_right_inverse_of_dimension line 35
  2. theorem OAI.Release061.ProjectionNashChart.right_inverse_at line 85
  3. theorem OAI.Release061.NashNormalCoordinates.graph_germ_at line 104
  4. def OAI.Release061.NashBoundaryChart.oldPosition line 121
  5. def OAI.Release061.NashBoundaryChart.oldParameter line 125
  6. def OAI.Release061.NashBoundaryChart.oldOffset line 128
  7. theorem OAI.Release061.NashBoundaryChart.oldParameter_oldPosition line 131
  8. theorem OAI.Release061.NashBoundaryChart.oldOffset_oldPosition line 135
  9. theorem OAI.Release061.NashBoundaryChart.oldOffset_analyticAt line 139
  10. theorem OAI.Release061.NashBoundaryChart.oldPosition_inverse line 147
  11. theorem OAI.Release061.NashBoundaryChart.oldPosition_projection line 152
  12. theorem OAI.Release061.NashBoundaryChart.oldOffset_projection_germ line 159