OAI/Geometry/RCD/Metric/EuclideanDyadicGrowthRigidity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Harmonic rigidity with only the dyadic bounds of the frame construction

  1. theorem OAI.RegularPointCoordinates.euclidean_harmonic_affine_of_dyadic_growth line 13