of_bases — Mathlib

English

If a space X has a neighborhood basis at each point consisting of path-connected sets, then X is LocPathConnectedSpace.

Русский

Если у пространства X есть базис окрестностей в каждой точке, состоящий из путепроходимых множеств, то X является локально путепроподобным пространством.

LaTeX

$$([basis], [IsPathConnected]) \rightarrow \text{LocPathConnectedSpace}(X)$$

Lean4

theorem of_bases {p : X → ι → Prop} {s : X → ι → Set X} (h : ∀ x, (𝓝 x).HasBasis (p x) (s x))
    (h' : ∀ x i, p x i → IsPathConnected (s x i)) : LocPathConnectedSpace X where
  path_connected_basis
    x := by
    rw [hasBasis_self]
    intro t ht
    rcases (h x).mem_iff.mp ht with ⟨i, hpi, hi⟩
    exact ⟨s x i, (h x).mem_of_mem hpi, h' x i hpi, hi⟩

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