OAI/Geometry/RCD/Sobolev/NestedBallCutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Explicit cutoffs between two concentric closed balls

  1. def OAI.RegularPointCoordinates.nestedBallCutoff line 15
  2. theorem OAI.RegularPointCoordinates.nestedBallCutoff_bounds line 18
  3. theorem OAI.RegularPointCoordinates.nestedBallCutoff_eq_one line 21
  4. theorem OAI.RegularPointCoordinates.nestedBallCutoff_eq_zero line 27
  5. theorem OAI.RegularPointCoordinates.nestedBallCutoff_lipschitz line 34
  6. theorem OAI.RegularPointCoordinates.nestedBallCutoff_tsupport line 52
  7. theorem OAI.RegularPointCoordinates.nestedBallCutoff_hasCompactSupport line 63