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

Commit

3 years ago

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

Author

urkud

urkud

Parents

Loading