English
If s is preconnected, f is injective and closed, and s ⊆ range f, then f^{-1}(s) is preconnected.
Русский
Если s предсвязно, f инъективно и замкнуто, и s ⊆ диапазон f, то прообраз предсвязно.
LaTeX
$$$\\mathrm{IsPreconnected}(s) \\Rightarrow \\mathrm{Injective}(f) \\Rightarrow \\mathrm{IsClosedMap}(f) \\Rightarrow s \\subseteq \\mathrm{range}(f) \\Rightarrow \\mathrm{IsPreconnected}(f^{-1}(s))$$$
Lean4
theorem preimage_of_isClosedMap [TopologicalSpace β] {s : Set β} (hs : IsPreconnected s) {f : α → β}
(hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ range f) : IsPreconnected (f ⁻¹' s) :=
isPreconnected_closed_iff.2 fun u v hu hv hsuv hsu hsv =>
by
replace hsf : f '' (f ⁻¹' s) = s := image_preimage_eq_of_subset hsf
obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty :=
by
refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
· simpa only [hsf, image_union] using image_mono (f := f) hsuv
· simpa only [image_preimage_inter] using hsu.image f
· simpa only [image_preimage_inter] using hsv.image f
· exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩
