OAI/Geometry/RCD/Metric/DerivativeValueCompactness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Derivative convergence from values and a common second-order bound

  1. theorem OAI.RegularPointCoordinates.deriv_forward_slope_bound line 13
  2. theorem OAI.RegularPointCoordinates.exists_derivative_limit_of_values line 24