Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lipschitz_with.maps_to_ball

Modification history

2022-02-24 14:38

src/topology/metric_space/lipschitz.lean

feat(topology/metric_space/lipschitz): add `set.maps_to` lemmas (#12266)

Added lipschitz_with.maps_to_ball View on Github →