CompactPhaseChart.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A single smooth inverse representative on a neighborhood of a compact phase-chart region, without changing its forward coordinate map.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.extend_compact_chart_inverse line 14