isOpen_isPathConnected_basis — Mathlib

English

For every x in X, the neighborhood filter at x has a basis consisting of open, path-connected neighborhoods of x.

Русский

Для каждой точки x пространство имеет базу окрестностей, состоящую из открытых путеподключённых окрестностей точки x.

LaTeX

$$(nhds x).HasBasis (fun s : Set X => IsOpen s ∧ x ∈ s ∧ IsPathConnected s) id$$

Lean4

theorem isOpen_isPathConnected_basis (x : X) :
    (𝓝 x).HasBasis (fun s : Set X ↦ IsOpen s ∧ x ∈ s ∧ IsPathConnected s) id :=
  by
  refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ mem_nhds_iff.mpr ⟨u, hu.2, hu.1.1, hu.1.2.1⟩⟩⟩
  have ⟨u, hus, hu, hxu⟩ := mem_nhds_iff.mp hs
  exact
    ⟨pathComponentIn u x, ⟨hu.pathComponentIn _, ⟨mem_pathComponentIn_self hxu, isPathConnected_pathComponentIn hxu⟩⟩,
      pathComponentIn_subset.trans hus⟩

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