OAI/Geometry/RCD/Coordinates/RadialFrameLocalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Localizing the actual normalizing frame to the radial testing region

  1. theorem OAI.RegularPointCoordinates.localize_radial_frame line 16