Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-17 23:53 7592a8f4

View on Github →

chore(analysis/normed_space/finite_dimension,topology/metric_space): golf (#6285)

  • golf two proofs about finite_dimension;
  • move proper_image_of_proper to antilipschitz, rename to antilipschitz_with.proper_space, golf.

Estimated changes