Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-29 21:58 be17b92a

View on Github →

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.

Estimated changes