OAI/Geometry/RCD/Metric/BoundedIsodiametric.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The sharp diameter bound for arbitrary bounded Euclidean sets

  1. theorem OAI.RegularPointCoordinates.bounded_isodiametric_of_compact line 12
  2. theorem OAI.RegularPointCoordinates.bounded_volume_le_diameter_pow line 22
  3. theorem OAI.RegularPointCoordinates.bounded_volume_le_ediam_pow line 33