locallyConnectedSpace_iff_subsets_isOpen_isConnected

English

LocallyConnectedSpace α is equivalent to the basis condition: for every x, nhds x has a basis of open connected sets containing x.

Русский

Локальная связность пространства эквивалентна условию базиса: для каждого x окрестности имеют базис открытых связных множеств, содержащихся в x.

LaTeX

$$LocallyConnectedSpace α ↔ ∀ x, (nhds x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id$$

Lean4

theorem locallyConnectedSpace_iff_subsets_isOpen_isConnected :
    LocallyConnectedSpace α ↔ ∀ x, ∀ U ∈ 𝓝 x, ∃ V : Set α, V ⊆ U ∧ IsOpen V ∧ x ∈ V ∧ IsConnected V :=
  by
  simp_rw [locallyConnectedSpace_iff_hasBasis_isOpen_isConnected]
  refine forall_congr' fun _ => ?_
  constructor
  · intro h U hU
    rcases h.mem_iff.mp hU with ⟨V, hV, hVU⟩
    exact ⟨V, hVU, hV⟩
  ·
    exact fun h =>
      ⟨fun U =>
        ⟨fun hU =>
          let ⟨V, hVU, hV⟩ := h U hU
          ⟨V, hV, hVU⟩,
          fun ⟨V, ⟨hV, hxV, _⟩, hVU⟩ => mem_nhds_iff.mpr ⟨V, hVU, hV, hxV⟩⟩⟩

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