OAI/Geometry/SurfaceImmersion/Primitive/ConstructedPrimitiveSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construct the smooth amplitude and the exact localized tensor of an actual surface primitive, retaining its precise geometric support.

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