OAI/Geometry/RCD/Heat/ScalingBoundaryLimit.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Uniform limits of the actual normalized endpoint scaling factors
- theorem
OAI.RegularPointCoordinates.NoncollapsedRCD.compact_scaling_boundary_limitline 18