connectedComponentIn_mem_nhds — Mathlib

English

In a locally path-connected space, if F ∈ 𝓝 x, then pathComponentIn F x ∈ 𝓝 x.

Русский

В пространстве с локальной путевой связностью, если F ∈ 𝓝 x, то pathComponentIn F x ∈ 𝓝 x.

LaTeX

$$pathComponentIn_mem_nhds$$

Lean4

theorem connectedComponentIn_mem_nhds [LocallyConnectedSpace α] {F : Set α} {x : α} (h : F ∈ 𝓝 x) :
    connectedComponentIn F x ∈ 𝓝 x :=
  by
  rw [(LocallyConnectedSpace.open_connected_basis x).mem_iff] at h
  rcases h with ⟨s, ⟨h1s, hxs, h2s⟩, hsF⟩
  exact mem_nhds_iff.mpr ⟨s, h2s.isPreconnected.subset_connectedComponentIn hxs hsF, h1s, hxs⟩

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