OAI/Geometry/RCD/Harmonic/BoundedTransverseFormula.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The bounded transverse test with its actual, possibly nonorthogonal, Gram entries
- theorem
OAI.RegularPointCoordinates.exists_bounded_transverse_formulaline 15