OAI/Geometry/SurfaceImmersion/Atlas/FixedAtlasSmallIncrement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Assemble an actual small increment from fixed geometric solvers and an adjusted mean.

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