Heine_Cantor_Theorem

Proved

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

compact-spacescontinuous-mappingsheine-cantor-theoremmetric-spacesproofwikiuniformly-continuous-mappings

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

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

theorem Heine_Cantor_Theorem {α : Type _} {β : Type _} [PseudoMetricSpace α] [PseudoMetricSpace β] [CompactSpace α] (f : α → β) (hf : Continuous f) : UniformContinuous f := by sorry

Source

https://proofwiki.org/wiki/Heine-Cantor_Theorem

View graph