English
Let X be a topological space, F a subset of X, and x an element of F. The path component of x in F is the set of all points y that lie in F and can be joined to x by a path contained in F. Equivalently, pathComponentIn(F, x) = { y ∈ X | JoinedIn(F, x, y) }.
Русский
Пусть X — топологическое пространство, F ⊆ X и x ∈ F. Компонента пути x в F — это множество точек y, которые лежат в F и могут быть соединены с x по кривой, лежащей внутри F. Эквивалентно: pathComponentIn(F, x) = { y ∈ X | JoinedIn(F, x, y) }.
LaTeX
$$$\mathrm{pathComponentIn}(F, x) = \{ y \in X \mid \text{JoinedIn}(F, x, y) \}$$$
Lean4
/-- The path component of `x` in `F` is the set of points that can be joined to `x` in `F`. -/
def pathComponentIn (F : Set X) (x : X) :=
{y | JoinedIn F x y}
