OAI/Geometry/SurfaceImmersion/Correction/CrossAtlasPolynomialTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite polynomial mean tensor is independent of the correction atlas.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_atlas_polynomial_transfer line 29