English
A subset s of a dependent sum is preconnected iff there exists i and a preconnected t with s = Σ i '' t.
Русский
Подмножество s зависимой суммы предсвязано тогда и только тогда, когда существует i и предсвязное t такое, что s = Σ i '' t.
LaTeX
$$$$IsPreconnected(s) \\iff \\exists i, t, IsPreconnected(t) \\land s = \\Sigma i '' t$$$$
Lean4
theorem isPreconnected_iff [hι : Nonempty ι] [∀ i, TopologicalSpace (X i)] {s : Set (Σ i, X i)} :
IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = Sigma.mk i '' t :=
by
refine ⟨fun hs => ?_, ?_⟩
· obtain rfl | h := s.eq_empty_or_nonempty
· exact ⟨Classical.choice hι, ∅, isPreconnected_empty, (Set.image_empty _).symm⟩
· obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩
exact ⟨a, t, ht.isPreconnected, rfl⟩
· rintro ⟨a, t, ht, rfl⟩
exact ht.image _ continuous_sigmaMk.continuousOn
