OAI/Geometry/RCD/Transport/RenyiLeftComponent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Maximality of a length component on the left 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_left_length_component_maximal line 22