Theorems · Theorem · general topology

ContractingWith.exists_fixedPoint

• 1000+ list: Banach fixed-point theorem

∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} [CompleteSpace α],
  ContractingWith K f →
    ∀ (x : α),
      edist x (f x) ≠ ⊤ →
        ∃ y,
          Function.IsFixedPt f y ∧
            Filter.Tendsto (fun n => f^[n] x) Filter.atTop (nhds y) ∧
              ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

Banach fixed-point theorem, contraction mapping theorem, EMetricSpace version. A contracting map on a complete metric space has a fixed point. We include more conclusions in this theorem to avoid proving them again later. The main API for this theorem are the functions efixedPoint and fixedPoint, and lemmas about these functions.

Defined in

Mathlib.Topology.MetricSpace.Contracting

Cited by

4 results in Mathlib

Foundations

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

Assumes

EMetricSpaceCompleteSpace