OAI/Geometry/RCD/Transport/ReducedDistortionNonpositive.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reduced-distortion interpolation including degenerate cases

  1. theorem OAI.RegularPointCoordinates.sigma_nonpos_interpolation line 11
  2. theorem OAI.RegularPointCoordinates.sigma_nonpos_zero line 30
  3. theorem OAI.RegularPointCoordinates.sigma_nonpos_one line 39