lipschitz): image of a bdd set (#11134)

Commit

3 years ago

feat(topology/metric_space/lipschitz): image of a bdd set (#11134) Prove that `f '' s` is bounded provided that `f` is Lipschitz continuous and `s` is bounded.

Author

urkud

Parents

5bfd9245

mathlib be17b92a - feat(topology/metric_space/lipschitz): image of a bdd set (#11134)

mathlib
be17b92a - feat(topology/metric_space/lipschitz): image of a bdd set (#11134)