totallyDisconnectedSpace — Mathlib

English

The subtype (Subtype p) is totally disconnected whenever α is TD.

Русский

Подтип (Subtype p) полностью раздельен тогда, когда исходное пространство TD.

LaTeX

$$TotallyDisconnectedSpace (Subtype p)$$

Lean4

instance totallyDisconnectedSpace {α : Type*} {p : α → Prop} [TopologicalSpace α] [TotallyDisconnectedSpace α] :
    TotallyDisconnectedSpace (Subtype p) :=
  totallyDisconnectedSpace_subtype_iff.2 (isTotallyDisconnected_of_totallyDisconnectedSpace _)

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