Topological_Product_of_Compact_Spaces

Proved

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

proofwikitopology

Let $T_1$ and $T_2$ be topological spaces. Let $T_1 \times T_2$ be the product space of $T_1$ and $T_2$ . Then $T_1 \times T_2$ is compact both $T_1$ and $T_2$ are compact.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Topological_Product_of_Compact_Spaces {α : Type _} {β : Type _} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [CompactSpace β] : CompactSpace (α × β) := by sorry

Source

https://proofwiki.org/wiki/Topological_Product_of_Compact_Spaces

View graph