OAI/Geometry/SurfaceImmersion/Primitive/CircularPrimitiveSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact analytic compact support and cutoff of a geometric circular primitive. In particular the support is the closed disk, not the atlas patch.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circular_primitive_support line 19