OAI/Geometry/RCD/Transport/RenyiRightComponent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Maximality of a length component on the right half

A competing half-plan is spliced into the full transport while keeping the original midpoint. The common length labels then give the disjointness needed to transfer midpoint maximality to the normalized component.

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