OAI/Geometry/RCD/Coordinates/FullSplittingCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Coordinates from product almost splitting

Huang--Huang (2024), Theorem 2.9(2), supplies the product approximation formulated by LocalAlmostSplittingInput. Sharp RCD packing removes its residual factor without assuming ambient flatness.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.full_splitting_coordinates line 20