feat(topology/metric_space/lipschitz): image of a bdd set (#11134)
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.





leanprover-community/mathlib,leanprover-community/mathlib