Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lipschitz_with_max

Modification history

2021-10-16 09:26

src/topology/metric_space/lipschitz.lean

feat(topology/metric_space/lipschitz): add `lipschitz_with.min` and `lipschitz_with.max` (#9744) …

Added lipschitz_with_max View on Github →