Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-16 08:03 9a11efbc

View on Github →

feat(metric_space): add lipschitz_on_with (#4151) The order of the explicit arguments in this definition is open for negotiation. From the sphere eversion project.

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem lipschitz_on_with.norm_sub_le

added theorem lipschitz_on_with_iff_norm_sub_le

Modified src/topology/metric_space/emetric_space.lean

added theorem emetric.uniform_continuous_on_iff

Modified src/topology/metric_space/lipschitz.lean

added theorem lipschitz_on_univ

added theorem lipschitz_on_with.mono

added def lipschitz_on_with

added theorem lipschitz_on_with_iff_dist_le_mul

added theorem lipschitz_on_with_iff_restrict

Modified src/topology/uniform_space/basic.lean

added theorem filter.has_basis.uniform_continuous_on_iff

added theorem uniform_continuous_on.continuous_on

modified theorem uniform_continuous_on_iff_restrict