OAI/Geometry/SurfaceImmersion/Whitney/DoubleLocusChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Smooth submersion coordinates for the three-component difference map on a pair of surface charts.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.double_locus_submersion_chart line 13