Module

ConnectedComponents.lean

Nyll.SchemeTheory.Topology.ConnectedComponents

1 declaration indexed from sourceView source ↗

Module documentation

Connected components of compact prespectral spaces

Compact open neighbourhoods and quasi-separatedness replace Hausdorff separation in the description of connected components as intersections of clopen neighbourhoods.

Imports5

Mathlib.Topology.Clopen
Mathlib.Topology.Compactness.Compact
Mathlib.Topology.Connected.Clopen
Mathlib.Topology.QuasiSeparated
Mathlib.Topology.Spectral.Prespectral

Imported by2

theorem

connectedComponent_eq_iInter_isClopen_of_prespectral

L36 ↗

SchemeTheory.connectedComponent_eq_iInter_isClopen_of_prespectral

Documentation

In a quasi-compact space with a basis of compact opens whose finite intersections are compact, each connected component is the intersection of its clopen neighbourhoods.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u
open Set TopologicalSpace
namespace SchemeTheory
variable {X : Type u} [TopologicalSpace X] [CompactSpace X]
  [PrespectralSpace X] [QuasiSeparatedSpace X]

Lean source · statement

theorem connectedComponent_eq_iInter_isClopen_of_prespectral (x : X) :
    connectedComponent x = ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s

Module documentation

Connected components of compact prespectral spaces

Declarations

connectedComponent_eq_iInter_isClopen_of_prespectral