Closed_Subspace_of_Compact_Space_is_Compact
Provedclosed-setscompact-spacesproofwiki
A closed subspace of a compact space is compact. That is, the property of being compact is weakly hereditary.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Closed_Subspace_of_Compact_Space_is_Compact {α : Type _} [TopologicalSpace α] [CompactSpace α] {s : Set α} (hs : IsClosed s) : IsCompact s := by sorrySource