pathComponent — Mathlib

English

In a locally path connected space, each path component is closed.

Русский

В локально путепроходимом пространстве каждая путепроходящая компонента замкнута.

LaTeX

$$IsClosed\pathComponent x$$

Lean4

/-- In a locally path connected space, each path component is a closed set. -/
protected theorem pathComponent (x : X) : IsClosed (pathComponent x) :=
  by
  rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
  intro y hxy
  rcases (path_connected_basis y).ex_mem with ⟨V, hVy, hVc⟩
  filter_upwards [hVy] with z hz hxz
  exact hxy <| hxz.trans (hVc.joinedIn _ hz _ (mem_of_mem_nhds hVy)).joined

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