OAI/Geometry/RCD/Coordinates/NormalizedSupportedCompression.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Restricting a normalized compression bound to its actual support

  1. theorem OAI.RegularPointCoordinates.normalized_supported_compression line 13