OAI/Geometry/CoveringDensity/EuclideanTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The coordinate map is a continuous linear equivalence and preserves volume. The Euclidean norm and the coordinate supremum norm need not agree.

  1. theorem OAI.CoveringOrder.euclidean_lattice_upper line 13