English
A subset s of a dependent sum Σ i, X_i is connected iff there exists an index i and a connected t ⊆ X_i with s = Σ i '' t.
Русский
Подмножество s зависимого суммы Σ i, X_i связано тогда и только тогда, когда существует индекс i и связное подмножество t ⊆ X_i с равенством s = Σ i '' t.
LaTeX
$$$$IsConnected(s) \\iff \\exists i, t, IsConnected(t) \\land s = \\Sigma i '' t$$$$
Lean4
theorem isConnected_iff [∀ i, TopologicalSpace (X i)] {s : Set (Σ i, X i)} :
IsConnected s ↔ ∃ i t, IsConnected t ∧ s = Sigma.mk i '' t :=
by
refine ⟨fun hs => ?_, ?_⟩
· obtain ⟨⟨i, x⟩, hx⟩ := hs.nonempty
have : s ⊆ range (Sigma.mk i) := hs.isPreconnected.subset_isClopen isClopen_range_sigmaMk ⟨⟨i, x⟩, hx, x, rfl⟩
exact
⟨i, Sigma.mk i ⁻¹' s, hs.preimage_of_isOpenMap sigma_mk_injective isOpenMap_sigmaMk this,
(Set.image_preimage_eq_of_subset this).symm⟩
· rintro ⟨i, t, ht, rfl⟩
exact ht.image _ continuous_sigmaMk.continuousOn
