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 ofefixed_point
and failed: every time I use it, it generates a goalcomplete_space ↥s
. So, I decided to deduceexists_fixed_point'
fromexists_fixed_point
, then use it in the proofs.