English
If f: X → Y is a function with coinduced topology, and X is locally path-connected, then Y is locally path-connected.
Русский
Если f: X → Y задать ководную топологию и X локально путеподключено, то Y тоже локально путеподключено.
LaTeX
$$LocPathConnectedSpace.coinduced {Y} (f) : LocPathConnectedSpace Y$$
Lean4
/-- Any topology coinduced by a locally path-connected topology is locally path-connected. -/
theorem coinduced {Y : Type*} (f : X → Y) : @LocPathConnectedSpace Y (.coinduced f ‹_›) :=
by
let _ := TopologicalSpace.coinduced f ‹_›; have hf : Continuous f := continuous_coinduced_rng
refine
locPathConnectedSpace_iff_isOpen_pathComponentIn.mpr fun y u hu ↦
isOpen_coinduced.mpr <| isOpen_iff_mem_nhds.mpr fun x hx ↦ ?_
have hx' := preimage_mono pathComponentIn_subset hx
refine
mem_nhds_iff.mpr ⟨pathComponentIn (f ⁻¹' u) x, ?_, (hu.preimage hf).pathComponentIn _, mem_pathComponentIn_self hx'⟩
rw [← image_subset_iff, ← pathComponentIn_congr hx]
exact
((isPathConnected_pathComponentIn hx').image hf).subset_pathComponentIn ⟨x, mem_pathComponentIn_self hx', rfl⟩ <|
(image_mono pathComponentIn_subset).trans <| u.image_preimage_subset f
