instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace

English

If X is noncompact and preconnected, then OnePoint X is a connected space.

Русский

Если X не компактно и предсоединено, то OnePoint X является связным пространством.

LaTeX

$$$\\text{ConnectedSpace}(\\mathrm{OnePoint}(X))$ for noncompact, preconnected X.$$

Lean4

/-- If `X` is not a compact space, then `OnePoint X` is a connected space. -/
instance [PreconnectedSpace X] [NoncompactSpace X] : ConnectedSpace (OnePoint X)
    where
  toPreconnectedSpace := isDenseEmbedding_coe.isDenseInducing.preconnectedSpace
  toNonempty := inferInstance

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