OAI/Geometry/RCD/Sobolev/MeasuredRadialCutoffSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Both radial cutoff representatives vanish outside one interior ball

  1. theorem OAI.RegularPointCoordinates.measured_radial_cutoff_zero_outside line 12