OAI/Geometry/RCD/Sobolev/InnerBallCutoffSequence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous inner approximations to a ball indicator

  1. theorem OAI.RegularPointCoordinates.inner_ball_lipschitz_cutoff_sequence line 14
  2. theorem OAI.RegularPointCoordinates.inner_ball_cutoff_sequence line 57