mathlib

9832fba5 - refactor(topology/metric_space/contracting): redefine using emetric (#2070)

refactor(topology/metric_space/contracting): redefine using emetric (#2070) * refactor(topology/metric_space/contracting): redefine using emetric * Fix a typo produced by "copy+paste" * Fix compile * Refactor `efixed_point`, `efixed_point'` * Prove a version of Banach fixed point theorem for a map contracting on a complete forward-invariant set. * Separately prove "primed" lemmas. I Tried to define `efixed_point'` in terms of `efixed_point` and failed: every time I use it, it generates a goal `complete_space ↥s`. So, I decided to deduce `exists_fixed_point'` from `exists_fixed_point`, then use it in the proofs. Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>