English
If s is preconnected, f is injective and an open map, and s ⊆ range f, then f^{-1}(s) is preconnected.
Русский
Если s предсвязно, f инъективно и открыто, и s ⊆ диапазон f, то прообраз предмножества предсвязно.
LaTeX
$$$\\mathrm{IsPreconnected}(s) \\Rightarrow \\mathrm{Injective}(f) \\Rightarrow \\mathrm{IsOpenMap}(f) \\Rightarrow s \\subseteq \\mathrm{range}(f) \\Rightarrow \\mathrm{IsPreconnected}(f^{-1}(s))$$$
Lean4
theorem preimage_of_isOpenMap [TopologicalSpace β] {f : α → β} {s : Set β} (hs : IsPreconnected s)
(hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ range f) : IsPreconnected (f ⁻¹' s) :=
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 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⟩
