OAI/Geometry/RCD/Metric/EuclideanBallHausdorffCost.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The diameter cost of a Euclidean ball and absolute continuity

  1. theorem OAI.RegularPointCoordinates.closedBall_ediam_le_twice line 13
  2. theorem OAI.RegularPointCoordinates.raw_hausdorff_absolutelyContinuous line 25
  3. theorem OAI.RegularPointCoordinates.euclidean_ball_diameter_cost line 34