SchemeTheory.t2Space_connectedComponents_of_prespectral
Clopen neighbourhoods separate distinct connected components of a compact quasi-separated prespectral space.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u
open Set TopologicalSpace
namespace SchemeTheoryLean source · statement
theorem t2Space_connectedComponents_of_prespectral {X : Type u} [TopologicalSpace X]
[CompactSpace X] [PrespectralSpace X] [QuasiSeparatedSpace X] :
T2Space (ConnectedComponents X)