isTotallyDisconnected_of_totallyDisconnectedSpace

English

If α is totally disconnected, then every subset s ⊆ α is totally disconnected (in the subspace topology).

Русский

Если пространство α полностью раздельно, то любую подмножество s ⊆ α можно рассматривать как полностью раздельное в топологии подпространства.

LaTeX

$$TotallyDisconnectedSpace(\alpha) \Rightarrow IsTotallyDisconnected(s)$$

Lean4

theorem isTotallyDisconnected_of_totallyDisconnectedSpace [TotallyDisconnectedSpace α] (s : Set α) :
    IsTotallyDisconnected s := fun t _ ht => TotallyDisconnectedSpace.isTotallyDisconnected_univ _ t.subset_univ ht

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