OAI/Geometry/RCD/Metric/ComponentHalfDistance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sharp half-distance bounds for a bounded-length component

Every optimal replacement of either half stays below half the component's length bound. The proof splices it into the parent transport and uses the common interior length label at the retained midpoint.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.component_splice_distance line 22