English
If H is locally path connected, then M is locally path connected.
Русский
Если H локально путево связно, то M локально путево связно.
LaTeX
$$[LocPathConnectedSpace H] => LocPathConnectedSpace M$$
Lean4
/-- If a topological space `M` admits an atlas with locally path-connected charts,
then `M` itself is locally path-connected. -/
theorem locPathConnectedSpace [LocPathConnectedSpace H] : LocPathConnectedSpace M :=
by
refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ Filter.mem_of_superset hu.1.1 hu.2⟩⟩⟩
let e := chartAt H x
let t := s ∩ e.source
have ht : t ∈ 𝓝 x := Filter.inter_mem hs (chart_source_mem_nhds _ _)
refine ⟨e.symm '' pathComponentIn (e '' t) (e x), ⟨?_, ?_⟩, (?_ : _ ⊆ t).trans inter_subset_left⟩
· nth_rewrite 1 [← e.left_inv (mem_chart_source _ _)]
apply e.symm.image_mem_nhds (by simp [e])
exact pathComponentIn_mem_nhds <| e.image_mem_nhds (mem_chart_source _ _) ht
· refine (isPathConnected_pathComponentIn <| mem_image_of_mem e (mem_of_mem_nhds ht)).image' ?_
refine e.continuousOn_symm.mono <| subset_trans ?_ e.map_source''
exact (pathComponentIn_mono <| image_mono inter_subset_right).trans pathComponentIn_subset
·
exact
(image_mono pathComponentIn_subset).trans
(PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).subset
