Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-23 14:57 9832fba5

View on Github →

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.

Estimated changes