English
If F is open, then for every x, the path component of F containing x is open in X.
Русский
Если F открыто, то для каждого x путь-компонента F, содержащая x, открыта в X.
LaTeX
$$IsOpen F \rightarrow \forall x, IsOpen( pathComponentIn F x )$$
Lean4
protected theorem pathComponentIn (hF : IsOpen F) (x : X) : IsOpen (pathComponentIn F x) :=
by
rw [isOpen_iff_mem_nhds]
intro y hy
let ⟨s, hs⟩ := (path_connected_basis y).mem_iff.mp (hF.mem_nhds (pathComponentIn_subset hy))
exact mem_of_superset hs.1.1 <| pathComponentIn_congr hy ▸ hs.1.2.subset_pathComponentIn (mem_of_mem_nhds hs.1.1) hs.2