lean_workbook_plus_3200

Proved

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

Let $(X,d)$ be some metric space, and let $f : X \to X$ be a continuous function. Will the function $g : X \to \Bbb{R}$ defined by $g(x) = d(f(x),x)$ be a continuous function? If so, prove it.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3200 (X : Type) [MetricSpace X]
  (f : X → X) (hf : Continuous f) : Continuous (λ x => dist (f x) x)   :=  by sorry

Source

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

View graph