OAI/Geometry/RCD/Harmonic/ContinuousApproximateRepresentative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

From almost everywhere to every point against an approximate map

  1. theorem OAI.RegularPointCoordinates.continuous_approximate_representative line 14