isTotallyDisconnected_of_isTotallySeparated

English

A pairwise separation property implies total disconnectedness for a subspace.

Русский

Свойство попарного разделения в подпространстве влечет полное раздельное пространство.

LaTeX

$$IsTotallySeparated s ⇒ IsTotallyDisconnected s$$

Lean4

theorem isTotallyDisconnected_of_isTotallySeparated {s : Set α} (H : IsTotallySeparated s) : IsTotallyDisconnected s :=
  by
  intro t hts ht x x_in y y_in
  by_contra h
  obtain ⟨u : Set α, v : Set α, hu : IsOpen u, hv : IsOpen v, hxu : x ∈ u, hyv : y ∈ v, hs : s ⊆ u ∪ v, huv⟩ :=
    H (hts x_in) (hts y_in) h
  refine (ht _ _ hu hv (hts.trans hs) ⟨x, x_in, hxu⟩ ⟨y, y_in, hyv⟩).ne_empty ?_
  rw [huv.inter_eq, inter_empty]

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