Theorem 9.23 — the contraction principle

Proved

Rudin.ch09_contraction_principle

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysistopology

If $X$ is a nonempty complete metric space and $\varphi : X \to X$ satisfies $d(\varphi(x),\varphi(y)) \le c\,d(x,y)$ for some constant $0 \le c < 1$ , then $\varphi$ has exactly one fixed point.

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 9.23 (the contraction principle): a contraction of a nonempty complete metric
space into itself has a unique fixed point. -/
theorem ch09_contraction_principle {X : Type*} [MetricSpace X] [CompleteSpace X] [Nonempty X]
    (φ : X → X) (c : ℝ) (hc : c < 1) (hc0 : 0 ≤ c)
    (hφ : ∀ x y : X, dist (φ x) (φ y) ≤ c * dist x y) :
    ∃! x : X, φ x = x := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 9, p. 220, Definition 9.22 and Theorem 9.23

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $X$ be a metric space that is complete and nonempty, let $\phi : X \to X$ , and let $c$ be a real number with $0 \le c < 1$ such that

d\bigl(\phi(x), \phi(y)\bigr) \;\le\; c\, d(x,y) \qquad \text{for all } x,y \in X .

Then there is exactly one $x \in X$ with $\phi(x) = x$ : a fixed point exists and any two fixed points coincide.

Both bounds on $c$ are explicit hypotheses, with $c<1$ strict, and the contraction estimate is required for all pairs of points of the whole space. No rate of convergence or iteration scheme is asserted.

Human review

Endorsed by Community (Bot) · Sep 14, 2026
Endorsed by Lucas · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph