English
If f is inducing, IsPreconnected(f[s]) is equivalent to IsPreconnected(s).
Русский
Если f индуктивно отображает, то предсвязность образа равна предсвязности исходного множества.
LaTeX
$$$[\\text{TopologicalSpace } \\beta] \\Rightarrow \\mathrm{IsInducing}(f) \\Rightarrow \\mathrm{IsPreconnected}(\\mathrm{Im}(f,s)) \\iff \\mathrm{IsPreconnected}(s)$$$
Lean4
theorem isPreconnected_image [TopologicalSpace β] {s : Set α} {f : α → β} (hf : IsInducing f) :
IsPreconnected (f '' s) ↔ IsPreconnected s :=
by
refine ⟨fun h => ?_, fun h => h.image _ hf.continuous.continuousOn⟩
rintro u v hu' hv' huv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩
rcases hf.isOpen_iff.1 hu' with ⟨u, hu, rfl⟩
rcases hf.isOpen_iff.1 hv' with ⟨v, hv, rfl⟩
replace huv : f '' s ⊆ u ∪ v := by rwa [image_subset_iff]
rcases h u v hu hv huv ⟨f x, mem_image_of_mem _ hxs, hxu⟩ ⟨f y, mem_image_of_mem _ hys, hyv⟩ with
⟨_, ⟨z, hzs, rfl⟩, hzuv⟩
exact
⟨z, hzs, hzuv⟩
/- TODO: The following lemmas about connection of preimages hold more generally for strict maps
(the quotient and subspace topologies of the image agree) whose fibers are preconnected. -/
