English
If H is locally connected, then M is locally connected.
Русский
Если у пространства H локально связные базы, то и M локально связное.
LaTeX
$$[LocallyConnectedSpace H] => LocallyConnectedSpace M$$
Lean4
/-- If a topological space admits an atlas with locally connected charts, then the space itself is
locally connected. -/
theorem locallyConnectedSpace [LocallyConnectedSpace H] : LocallyConnectedSpace M :=
by
let e : M → OpenPartialHomeomorph M H := chartAt H
refine
locallyConnectedSpace_of_connected_bases (fun x s ↦ (e x).symm '' s)
(fun x s ↦ (IsOpen s ∧ e x x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) ?_ ?_
· intro x
simpa only [e, OpenPartialHomeomorph.symm_map_nhds_eq, mem_chart_source] using
((LocallyConnectedSpace.open_connected_basis (e x x)).restrict_subset
((e x).open_target.mem_nhds (mem_chart_target H x))).map
(e x).symm
· rintro x s ⟨⟨-, -, hsconn⟩, hssubset⟩
exact hsconn.isPreconnected.image _ ((e x).continuousOn_symm.mono hssubset)
