OAI/Geometry/SurfaceImmersion/Correction/AtlasPolynomialCoordinateRead.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A polynomial in one localized atlas map has an actual finite jet expression in another chart, on the nonzero partition-weight locus.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.compact_polynomial_coordinate_read line 21