totallyDisconnectedSpace — Mathlib

English

If X ≃ Y and X is totally disconnected, then Y is totally disconnected as well.

Русский

Если X гомеоморфно Y и X полностью несвязное, то и Y также полностью несвязное.

LaTeX

$$$TotallyDisconnectedSpace X \\Rightarrow TotallyDisconnectedSpace Y$$$

Lean4

protected theorem totallyDisconnectedSpace (h : X ≃ₜ Y) [tdc : TotallyDisconnectedSpace X] :
    TotallyDisconnectedSpace Y :=
  (totallyDisconnectedSpace_iff Y).mpr (h.range_coe ▸ ((IsEmbedding.isTotallyDisconnected_range h.isEmbedding).mpr tdc))

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