mem_pathComponent — Mathlib

English

Let X be a topological space. If y and z can be joined by a path, and y lies in the path component of x, then z also lies in the path component of x.

Русский

Пусть X — топологическое пространство. Если между y и z существует путь, и y принадлежит компоненте пути x, то и z принадлежит компоненте пути x.

LaTeX

$$$$\forall x,y,z \in X:\ \Big(\exists \gamma:[0,1]\to X,\ \gamma(0)=y \land \gamma(1)=z\Big) \land y \in \operatorname{pathComponent}(x) \Rightarrow z \in \operatorname{pathComponent}(x).$$$$

Lean4

theorem mem_pathComponent (hyz : Joined y z) (hxy : y ∈ pathComponent x) : z ∈ pathComponent x :=
  hxy.trans hyz

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