Commit 2020-03-23 14:57 9832fba5

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.