ProfiniteSpace.lean

theorem isTopologicalBasis_isClopen_of_compact_t2_totallyDisconnected {X : Type w}
    [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] :
    TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}

theorem exists_clopen_subset_of_mem_open {X : Type w} [TopologicalSpace X]
    [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
    {x : X} {U : Set X} (hU : IsOpen U) (hx : x ∈ U) :
    ∃ V : Set X, IsClopen V ∧ x ∈ V ∧ V ⊆ U

def discreteQuotientSystem (X : Type w) [TopologicalSpace X] :
    InverseSystem (I := OrderDual (DiscreteQuotient X)) where
  X := fun Q => Quotient (show DiscreteQuotient X from Q).toSetoid
  topologicalSpace := fun _ => inferInstance
  map := fun {Q R} h => DiscreteQuotient.ofLE h
  continuous_map := fun {Q R} _ => continuous_of_discreteTopology
  map_id := fun Q => by
    funext x
    exact DiscreteQuotient.ofLE_refl_apply (A := (Q : DiscreteQuotient X)) x
  map_comp := fun {Q R T} hQR hRT => by
    funext x
    exact congrFun (DiscreteQuotient.ofLE_comp_ofLE hRT hQR) x

theorem compatibleMaps_discreteQuotientProj (X : Type w) [TopologicalSpace X] :
    (discreteQuotientSystem X).CompatibleMaps
      (fun Q : OrderDual (DiscreteQuotient X) => (Q : DiscreteQuotient X).proj) := by
  intro Q R h
  funext x
  exact DiscreteQuotient.ofLE_proj h x

def homeomorph_inverseLimit_discreteQuotientSystem (X : Type w)
    [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] :
    X ≃ₜ (discreteQuotientSystem X).inverseLimit

theorem discreteQuotientSystem_projection_homeomorph (X : Type w)
    [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
    (Q : OrderDual (DiscreteQuotient X)) (x : X) :
    (discreteQuotientSystem X).projection Q
        (homeomorph_inverseLimit_discreteQuotientSystem X x) =
      (show DiscreteQuotient X from Q).proj x := by
  let S := discreteQuotientSystem X
  change (S.inverseLimitLift (fun Q : OrderDual (DiscreteQuotient X) =>
      (show DiscreteQuotient X from Q).proj)
      (compatibleMaps_discreteQuotientProj X) x).1 Q =
    (show DiscreteQuotient X from Q).proj x
  rfl

theorem totallyDisconnectedSpace_of_t2_basis_clopen (X : Type w) [TopologicalSpace X] [T2Space X]
    (hX : TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}) :
    TotallyDisconnectedSpace X