OAI/Geometry/RCD/Metric/RationalInteriorBalls.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A countable compact exhaustion of each open metric ball

  1. theorem OAI.RegularPointCoordinates.ball_eq_iUnion_rational_closedBall line 14