OAI/Geometry/RCD/Metric/CommonMeasuredApproximations.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The published measured-coordinate input on one common sequence of maps

  1. theorem OAI.RegularPointCoordinates.LocalMeasuredCoordinateInput.common_approximations line 15