Continuous_Image_of_Compact_Space_is_Compact

Proved

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

compact-spacescontinuous-invariantsproofwiki

Let $T_1$ and $T_2$ be topological spaces. Let $f: T_1 \to T_2$ be a continuous mapping. If $T_1$ is compact then so is its image $f \sqbrk {T_1}$ under $f$ . That is, compactness is a continuous invariant.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Continuous_Image_of_Compact_Space_is_Compact {α : Type _} {β : Type _} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) {s : Set α} (hs : IsCompact s) : IsCompact (f '' s) := by sorry

Source

https://proofwiki.org/wiki/Continuous_Image_of_Compact_Space_is_Compact

View graph