OAI/Geometry/RCD/Sobolev/RightSlopeCorrection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A first-order correction retained in a one-sided comparison

  1. theorem OAI.RegularPointCoordinates.right_slope_correction_le line 11