OAI/Geometry/RCD/Coordinates/DyadicRootEventualSplitting.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The prescribed root frame eventually satisfies every fixed splitting tolerance

  1. theorem OAI.RegularPointCoordinates.dyadic_root_eventual_splitting line 15