OAI/Geometry/EinsteinFour/MetricChartLipschitz.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The chart map is Lipschitz on a sufficiently small Riemannian ball. Short paths between points of the smaller ball stay in the neighborhood where the chart differential is bounded.

  1. theorem OAI.PositiveEinsteinFour.Geometry.iInf_open_interval line 22

    Also declared: OAI/Geometry/EinsteinFour/WeylEstimates03.lean:1952 (same declaration text).

  2. theorem OAI.PositiveEinsteinFour.Geometry.exists_metric_chart_lipschitz line 32