borel-baire-quotient-background
ProvedQAlgorithms.Papers.Independent.Intakethird100.P20.baire_of_locally_compact_or_completeprove2quantum
Every locally compact Hausdorff space is a Baire space, and every complete metric space is a Baire space. Empty spaces are allowed. The Hausdorff convention comes from the source paragraph immediately preceding the claim.
Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20
Formal statement
noncomputable section
namespace QAlgorithms.Papers.Independent.Intakethird100.P20
open Set TopologicalSpace
open QAlgorithms.Papers.Independent.Next46.P33 (Projection)
open scoped Topology
universe u v
/-- borel-baire-quotient-background; de Groote, Observables I, PDF pp. 52.
Restored in moderation: source background status is not a formalization obstacle. -/
theorem baire_of_locally_compact_or_complete :
(∀ (M : Type u) [TopologicalSpace M] [T2Space M] [LocallyCompactSpace M], BaireSpace M) ∧
(∀ (M : Type u) [MetricSpace M] [CompleteSpace M], BaireSpace M) := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P20
end
Source
Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 52, borel-baire-quotient-background
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
Both of the following universal assertions hold: every topological space that is Hausdorff and locally compact is a Baire space, and every metric space that is complete is a Baire space. Here being a Baire space means that every countable intersection of dense open subsets is dense. Neither assertion requires to be nonempty.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.