OAI/Geometry/EinsteinFour/ChartMetricSmoothness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Smoothness of the actual pulled-back metric in a chart. The tangent vectors are transported by the derivative of the inverse chart.

  1. theorem OAI.PositiveEinsteinFour.Geometry.chart_inverse_vector_smooth line 20
  2. theorem OAI.PositiveEinsteinFour.Geometry.metricInChart_contDiffOn line 40
  3. theorem OAI.PositiveEinsteinFour.Geometry.metricInChart_contDiffAt line 48
  4. theorem OAI.PositiveEinsteinFour.Geometry.matrix_det_smooth_at line 54
  5. theorem OAI.PositiveEinsteinFour.Geometry.matrix_inverse_entry_smooth_at line 62
  6. theorem OAI.PositiveEinsteinFour.Geometry.christoffel_contDiffAt line 80
  7. theorem OAI.PositiveEinsteinFour.Geometry.metricInChart_inv_contDiffAt line 95