connectedComponent_eq_univ — Mathlib

English

In a preconnected space, for every x, its connected component is the whole space.

Русский

В предсвязном пространстве для любой точки компонентa связности равна всему пространству.

LaTeX

$$$$\\text{connectedComponent}(x) = \\mathrm{univ}$$$$

Lean4

@[simp]
theorem connectedComponent_eq_univ {X : Type*} [TopologicalSpace X] [h : PreconnectedSpace X] (x : X) :
    connectedComponent x = univ :=
  preconnectedSpace_iff_connectedComponent.mp h x

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