isPathConnected_pathComponent — Mathlib

English

Let X be a topological space and x ∈ X. Then the path component of x is path-connected.

Русский

Пусть X — топологическое пространство и x ∈ X. Множество pathComponent(x) пути-связно для x.

LaTeX

$$$\mathrm{IsPathConnected}(\mathrm{pathComponent}(x))$$$

Lean4

theorem isPathConnected_pathComponent : IsPathConnected (pathComponent x) :=
  by
  rw [← pathComponentIn_univ]
  exact isPathConnected_pathComponentIn (mem_univ x)

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