OAI/Geometry/RCD/Sobolev/DimensionalCutoffLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One-sided slopes from dimensional cutoff secants

  1. theorem OAI.RegularPointCoordinates.frequent_right_slope_of_limiting_secants line 11
  2. theorem OAI.RegularPointCoordinates.frequent_slope_of_dimensional_cutoffs line 28