English
Let X be a locally path-connected space. If F is a neighborhood of x (i.e., F ∈ 𝓝(x)), then the path component of x in F is a neighborhood of x; that is, pathComponentIn(F, x) ∈ 𝓝(x).
Русский
Пусть X — пространство с локально путевой связностью. Если F является окрестностью точки x (F ∈ 𝓝(x)), то путь-компонента x внутри F является окрестностью x; то есть pathComponentIn(F, x) ∈ 𝓝(x).
LaTeX
$$$\\forall x \\in X\\,\\forall F \\subseteq X,\\ F \\in \\mathcal{N}(x) \\Rightarrow \\ pathComponentIn F x \\in \\mathcal{N}(x)$$$
Lean4
theorem pathComponentIn_mem_nhds (hF : F ∈ 𝓝 x) : pathComponentIn F x ∈ 𝓝 x :=
by
let ⟨u, huF, hu, hxu⟩ := mem_nhds_iff.mp hF
exact
mem_nhds_iff.mpr ⟨pathComponentIn u x, pathComponentIn_mono huF, hu.pathComponentIn x, mem_pathComponentIn_self hxu⟩
