Theorems · Definition · general topology

ContractingWith.efixedPoint

{α : Type u_1} →
  [inst : EMetricSpace α] →
    {K : NNReal} → (f : α → α) → [CompleteSpace α] → ContractingWith K f → (x : α) → edist x (f x) ≠ ⊤ → α

Let x be a point of a complete emetric space. Suppose that f is a contracting map, and edist x (f x) ≠ ∞. Then efixedPoint is the unique fixed point of f in Metric.eball x ∞.

Defined in

Mathlib.Topology.MetricSpace.Contracting

Cited by

7 results in Mathlib

Foundations

Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EMetricSpaceCompleteSpace