English
The image of a preconnected set is preconnected, provided the ambient topology allows it.
Русский
Образ предсвязного множества предсвязен при подходящей топологии окружения.
LaTeX
$$$\\mathrm{IsPreconnected}(s) \\Rightarrow \\text{(for } f:\\alpha\\to\\beta\\text{) ContinuousOn}(f,s) \\Rightarrow \\mathrm{IsPreconnected}(f''s)$$$
Lean4
/-- The image of a preconnected set is preconnected as well. -/
protected theorem image [TopologicalSpace β] {s : Set α} (H : IsPreconnected s) (f : α → β) (hf : ContinuousOn f s) :
IsPreconnected (f '' s) := by
-- Unfold/destruct definitions in hypotheses
rintro u v hu hv huv ⟨_, ⟨x, xs, rfl⟩, xu⟩ ⟨_, ⟨y, ys, rfl⟩, yv⟩
rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩
rcases continuousOn_iff'.1 hf v hv with
⟨v', hv', v'_eq⟩
-- Reformulate `huv : f '' s ⊆ u ∪ v` in terms of `u'` and `v'`
replace huv : s ⊆ u' ∪ v' := by
rw [image_subset_iff, preimage_union] at huv
replace huv := subset_inter huv Subset.rfl
rw [union_inter_distrib_right, u'_eq, v'_eq, ← union_inter_distrib_right] at huv
exact
(subset_inter_iff.1 huv).1
-- Now `s ⊆ u' ∪ v'`, so we can apply `‹IsPreconnected s›`
obtain ⟨z, hz⟩ : (s ∩ (u' ∩ v')).Nonempty :=
by
refine H u' v' hu' hv' huv ⟨x, ?_⟩ ⟨y, ?_⟩ <;> rw [inter_comm]
exacts [u'_eq ▸ ⟨xu, xs⟩, v'_eq ▸ ⟨yv, ys⟩]
rw [← inter_self s, inter_assoc, inter_left_comm s u', ← inter_assoc, inter_comm s, inter_comm s, ← u'_eq, ←
v'_eq] at hz
exact ⟨f z, ⟨z, hz.1.2, rfl⟩, hz.1.1, hz.2.1⟩
