English
The connected component of x in F is defined by taking the image of the connected component of x in the subtype F when x ∈ F, otherwise it is empty.
Русский
Связанная компонента x в F равна образу связной компоненты (x) в подмножество F, если x ∈ F, иначе пустое.
LaTeX
$$$\\text{connectedComponentIn}(F,x) = \\begin{cases} (\\uparrow)''\\mathrm{connectedComponent}(\\langle x, x\\in F \\rangle) & \\text{если } x\\in F, \\\\ \\emptyset & \\text{иначе} \\end{cases}$$$
Lean4
/-- Given a set `F` in a topological space `α` and a point `x : α`, the connected
component of `x` in `F` is the connected component of `x` in the subtype `F` seen as
a set in `α`. This definition does not make sense if `x` is not in `F` so we return the
empty set in this case. -/
def connectedComponentIn (F : Set α) (x : α) : Set α :=
if h : x ∈ F then (↑) '' connectedComponent (⟨x, h⟩ : F) else ∅
