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⟩