Theorem B.9

Proved

QAlgorithms.Papers.Independent.Intakethird100.P07.closedSubspace_isKSpace

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $X$ be a compactly Hausdorff generated space and $A\subseteq X$ a closed subset with the induced topology. Then

A\text{ is compactly Hausdorff generated}.

The ambient space and the closed subspace need not satisfy a Hausdorff axiom. The empty closed subset is allowed.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P07

Formal statement

noncomputable section

universe u v

namespace QAlgorithms.Papers.Independent.Intakethird100.P07

open CategoryTheory Topology TopologicalSpace

/-- Theorem B.9, PDF pp. 36–37: every closed subspace of a k-space is a
k-space. No Hausdorff axiom is imposed on the ambient space. -/
theorem closedSubspace_isKSpace
    (X : Type u) [TopologicalSpace X] [UCompactlyGeneratedSpace.{u} X]
    (A : Set X) (hA : IsClosed A) : UCompactlyGeneratedSpace.{u} A := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P07

end

Source

Cohomology of Local Cochains, arXiv:1110.2661v2, PDF p. 36, Theorem B.9

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every topological space $X$ whose underlying type lies in universe $u$ , assume that its topology is detected by continuous maps from compact Hausdorff spaces in universe $u$ : a subset $U\subseteq X$ is open if and only if $p^{-1}(U)$ is open for every such space $K$ and every continuous map $p:K\to X$ . For every closed subset $A\subseteq X$ , the subspace topology on $A$ has the same property: a subset $V\subseteq A$ is open if and only if $r^{-1}(V)$ is open for every compact Hausdorff space $K$ in universe $u$ and every continuous map $r:K\to A$ . This includes $A=\varnothing$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph