OAI/Geometry/RCD/Transport/QuadraticMidpointSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous midpoint laws from a countable family of distance tests

  1. theorem OAI.RegularPointCoordinates.quadratic_midpoint_selection line 16