Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-29 13:17 8ee4f2da

View on Github →

move continuous_of_lipschitz around

Estimated changes

Modified src/topology/bounded_continuous_function.lean

deleted theorem continuous_of_lipschitz

Modified src/topology/metric_space/lipschitz.lean

added theorem continuous_of_lipschitz

added theorem uniform_continuous_of_le_add

added theorem uniform_continuous_of_lipschitz