OAI/Geometry/RCD/Transport/LengthComponentDyadic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Whole length components inherit all dyadic maximality

Half-subpath restriction rescales the length label. The endpoint speed identity therefore transfers every level of the actual variational tree.

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