Equivalence_of_Definitions_of_Continuity_on_Metric_Spaces

Proved

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

continuous-mappings-on-metric-spacesproofwiki

Let $M_1 = \left({A_1, d_1}\right)$ and $M_2 = \left({A_2, d_2}\right)$ be metric spaces. Let $f: A_1 \to A_2$ be a mapping from $A_1$ to $A_2$ .

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

theorem Equivalence_of_Definitions_of_Continuity_on_Metric_Spaces {α : Type _} {β : Type _} [MetricSpace α] [MetricSpace β] (f : α → β) : (∀ x, ∀ ε > 0, ∃ δ > 0, ∀ y, dist x y < δ → dist (f x) (f y) < ε) ↔ Continuous f := by sorry

Source

https://proofwiki.org/wiki/Equivalence_of_Definitions_of_Continuity_on_Metric_Spaces

View graph