toLocallyConnectedSpace — Mathlib

English

A space with discrete topology is locally connected (hence locally path-connected).

Русский

Пространство с дискретной топологией локально связано (следовательно, локально путеподключено).

LaTeX

$$DiscreteTopology.toLocallyConnectedSpace$$

Lean4

/-- A space with discrete topology is a locally connected space. -/
instance (priority := 100) toLocallyConnectedSpace (α) [TopologicalSpace α] [DiscreteTopology α] :
    LocallyConnectedSpace α :=
  locallyConnectedSpace_iff_subsets_isOpen_isConnected.2 fun x _U hU =>
    ⟨{ x }, singleton_subset_iff.2 <| mem_of_mem_nhds hU, isOpen_discrete _, rfl, isConnected_singleton⟩

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