mathlib

aa35f363 - feat(analysis/hofer): Hofer's lemma (#3064)

feat(analysis/hofer): Hofer's lemma (#3064) Adds Hofer's lemma about complete metric spaces, with supporting material. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>