pathConnected_subset_basis — Mathlib

English

Let U be an open set and x ∈ U. Then the neighborhood filter at x has a basis consisting of path-connected subsets contained in U; in particular, there exist neighborhoods of x that are path-connected and lie inside U.

Русский

Пусть U — открытое множество и x ∈ U. Тогда вокруг x существует база окрестностей из путеподключённых подмножеств, содержащихся в U.

LaTeX

$$$(\\mathcal{N} x).HasBasis (\\lambda s \\;:\\ Set X,\\ s \\in \\mathcal{N} x \\land IsPathConnected s \\land s \\subseteq U) id$$$

Lean4

theorem pathConnected_subset_basis {U : Set X} (h : IsOpen U) (hx : x ∈ U) :
    (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 x ∧ IsPathConnected s ∧ s ⊆ U) id :=
  (path_connected_basis x).hasBasis_self_subset (IsOpen.mem_nhds h hx)

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