loc_compact_t2_tot_disc_iff_tot_sep

English

For a compact, totally disconnected, Hausdorff space, the neighborhood basis at a point x can be taken to consist of sets that are both closed and open (clopen).

Русский

В компактном хаусдорфовом полностью несвязном пространстве базис окрестностей состоит из множеств, которые одновремено замкнуты и открыты.

LaTeX

$$$\\nhds(x)$ has a basis consisting of clopen neighborhoods of x.$$

Lean4

/-- A locally compact Hausdorff space is totally disconnected
  if and only if it is totally separated. -/
theorem loc_compact_t2_tot_disc_iff_tot_sep : TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H :=
  by
  constructor
  · intro h
    exact totallySeparatedSpace_of_t0_of_basis_clopen loc_compact_Haus_tot_disc_of_zero_dim
  apply TotallySeparatedSpace.totallyDisconnectedSpace

Похожие утверждения