English
A more general form: if Y is locally connected, and h is a homeomorphism, then X is locally connected.
Русский
Более обобщенно: если Y локально связно и есть гомеоморфизм h, то X локально связано.
LaTeX
$$$LocallyConnectedSpace X$ given $h:X\\simeq Y$ and $LocallyConnectedSpace Y$$$
Lean4
/-- If the codomain of a homeomorphism is a locally connected space, then the domain is also
a locally connected space. -/
theorem locallyConnectedSpace [i : LocallyConnectedSpace Y] (h : X ≃ₜ Y) : LocallyConnectedSpace X :=
by
have : ∀ x, (𝓝 x).HasBasis (fun s ↦ IsOpen s ∧ h x ∈ s ∧ IsConnected s) (h.symm '' ·) := fun x ↦
by
rw [← h.symm_map_nhds_eq]
exact (i.1 _).map _
refine locallyConnectedSpace_of_connected_bases _ _ this fun _ _ hs ↦ ?_
exact hs.2.2.2.image _ h.symm.continuous.continuousOn
