Compact_Subspace_of_Hausdorff_Space_is_Closed

Proved

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

closed-setscompact-spacescompact-subspace-of-hausdorff-space-is-closedhausdorff-spacesproofwikitopological-subspaces

Let $H = \struct {A, \tau}$ be a Hausdorff space. Let $C$ be a compact subspace of $H$ . Then $C$ is closed in $H$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Compact_Subspace_of_Hausdorff_Space_is_Closed {α : Type _} [TopologicalSpace α] [T2Space α] {s : Set α} (hs : IsCompact s) : IsClosed s := by sorry

Source

https://proofwiki.org/wiki/Compact_Subspace_of_Hausdorff_Space_is_Closed

View graph