OAI/Geometry/EinsteinFour/MetricChartDistance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A bounded inverse-chart differential controls the actual Riemannian distance on a convex chart region. This is the local estimate needed for finiteness of the metric's Hausdorff volume.

  1. theorem OAI.PositiveEinsteinFour.Geometry.metricEDistance_chart_symm_le line 23
  2. theorem OAI.PositiveEinsteinFour.Geometry.exists_metric_chart_bound line 83