English
If all spaces X i are topological, and each s i is preconnected, then the univ-valued pi is preconnected.
Русский
Если все пространства X_i топологичны и каждое s_i предсвязно, то произведение по i (univ.pi s) предсвязно.
LaTeX
$$$\\forall i, \\mathrm{IsPreconnected}(s(i)) \\Rightarrow \\mathrm{IsPreconnected}(\\text{univ.pi } s)$$$
Lean4
theorem isPreconnected_univ_pi [∀ i, TopologicalSpace (X i)] {s : ∀ i, Set (X i)} (hs : ∀ i, IsPreconnected (s i)) :
IsPreconnected (pi univ s) := by
rintro u v uo vo hsuv ⟨f, hfs, hfu⟩ ⟨g, hgs, hgv⟩
classical
rcases exists_finset_piecewise_mem_of_mem_nhds (uo.mem_nhds hfu) g with ⟨I, hI⟩
induction I using Finset.induction_on with
| empty =>
refine ⟨g, hgs, ⟨?_, hgv⟩⟩
simpa using hI
| insert i I _ ihI =>
rw [Finset.piecewise_insert] at hI
have := I.piecewise_mem_set_pi hfs hgs
refine (hsuv this).elim ihI fun h => ?_
set S := update (I.piecewise f g) i '' s i
have hsub : S ⊆ pi univ s := by
refine image_subset_iff.2 fun z hz => ?_
rwa [update_preimage_univ_pi]
exact fun j _ => this j trivial
have hconn : IsPreconnected S := (hs i).image _ (continuous_const.update i continuous_id).continuousOn
have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩
have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩
refine (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono ?_
exact inter_subset_inter_left _ hsub
