English
If F is path-connected and f is continuous on F, then the image f(F) is path-connected.
Русский
Если F связно по траекториям и функция f непрерывна на F, тогда образ f(F) связан по траекториям.
LaTeX
$$$$\text{If }\text{IsPathConnected}(F) \text{ and } f\text{ continuous on }F, \text{ then } \operatorname{image}(f,F) \text{ is path-connected}.$$$$
Lean4
/-- If `f` is continuous on `F` and `F` is path-connected, so is `f(F)`. -/
theorem image' (hF : IsPathConnected F) {f : X → Y} (hf : ContinuousOn f F) : IsPathConnected (f '' F) :=
by
rcases hF with ⟨x, x_in, hx⟩
use f x, mem_image_of_mem f x_in
rintro _ ⟨y, y_in, rfl⟩
refine ⟨(hx y_in).somePath.map' ?_, fun t ↦ ⟨_, (hx y_in).somePath_mem t, rfl⟩⟩
exact hf.mono (range_subset_iff.2 (hx y_in).somePath_mem)
