OAI/Geometry/RCD/Harmonic/BoundedTransversePotentials.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded axial and transverse potentials before imposing any Gram identities

  1. theorem OAI.RegularPointCoordinates.bounded_transverse_potentials line 14