Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lipschitz_with.proper_space

Modification history

2023-01-24 03:14
src/topology/metric_space/antilipschitz.lean
refactor(analysis/complex/basic, data/complex/is_R_or_C): downgrade imports (#18217) …
Added lipschitz_with.proper_spaceView on Github →