mem_pathComponent — Mathlib

English

If F is path-connected, then every y ∈ F lies in the path component of every x ∈ F.

Русский

Если F связано по траекториям, то любой y ∈ F лежит в компоненте пути x для любого x ∈ F.

LaTeX

$$$$\forall x,y \in F:\ y \in \operatorname{pathComponent}(x).$$$$

Lean4

theorem mem_pathComponent (h : IsPathConnected F) (x_in : x ∈ F) (y_in : y ∈ F) : y ∈ pathComponent x :=
  (h.joinedIn x x_in y y_in).joined

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