Module

CountableModels.lean

Nyll.ProCGroups.InverseSystems.CountableModels

2 declarations indexed from sourceView source ↗

Module documentation

Countable inverse-system models of profinite spaces

A second-countable profinite space is represented as an inverse limit of a sequence of finite discrete spaces. Conversely, the module characterizes second countability by the existence of a finite-discrete inverse-system presentation over a countable linear order.

Imports4

Mathlib.Data.Set.Countable
Mathlib.Topology.ClopenBox
Mathlib.Topology.DiscreteQuotient
Nyll.ProCGroups.InverseSystems.ProfiniteSpace

Imported by1

Nyll.ProCGroups.InverseSystems.All

theorem

exists_nat_inverseSystem_of_secondCountable

L28 ↗

ProCGroups.InverseSystems.exists_nat_inverseSystem_of_secondCountable

Documentation

A second-countable profinite space is a sequential inverse limit of finite discrete spaces.

Source context 4 commands

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

open Set
open scoped Topology
namespace ProCGroups.InverseSystems
universe u w

Lean source · statement

theorem exists_nat_inverseSystem_of_secondCountable (X : Type w) [TopologicalSpace X]
    [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
    [SecondCountableTopology X] :
    ∃ S : InverseSystem.{0, w} (I := ℕ),
      (∀ n, Finite (S.X n)) ∧ (∀ n, DiscreteTopology (S.X n)) ∧
      Nonempty (X ≃ₜ S.inverseLimit)

theorem

secondCountable_iff_exists_countableLinearOrder_finiteDiscreteInverseSystem

L99 ↗

ProCGroups.InverseSystems.secondCountable_iff_exists_countableLinearOrder_finiteDiscreteInverseSystem