pathComponent_eq_connectedComponent

English

In a locally path-connected space, for every x the path component of x in the whole space equals the connected component of x.

Русский

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

LaTeX

$$pathComponent x = connectedComponent x$$

Lean4

theorem pathComponent_eq_connectedComponent (x : X) : pathComponent x = connectedComponent x :=
  (pathComponent_subset_component x).antisymm <|
    (IsClopen.pathComponent x).connectedComponent_subset (mem_pathComponent_self _)

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