lean_workbook_plus_3721

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $f : X \to X$ be such that $d(f(x),f(y)) \le a d(x,y)$ for every $x,y \in X$ for some $a \in (0,1)$ . Show that $g(x) = d(f(x),x)$ is continuous.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3721 (X : Type*) [MetricSpace X]
  (α : ℝ) (hα : 0 < α ∧ α < 1) (f : X → X) (hf : ∀ x y, dist (f x) (f y) ≤ α * dist x y) :
  Continuous (λ x => dist (f x) x)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph