English
A subset s of the disjoint sum α ⊕ β is connected iff it lies entirely in the left copy or entirely in the right copy, with the corresponding piece connected.
Русский
Подмножество s из непересекаемой суммы α ⊕ β связано тогда и только тогда, когда оно целиком лежит в левой копии или в правой копии, причём соответствующая часть связана.
LaTeX
$$$$IsConnected(s) \iff \\Big(\\exists t, IsConnected(t) \\land s = \\mathrm{Sum.inl} '' t\\Big) \\lor \\Big(\\exists t, IsConnected(t) \\land s = \\mathrm{Sum.inr} '' t\\Big)$$$$
Lean4
theorem isConnected_iff [TopologicalSpace β] {s : Set (α ⊕ β)} :
IsConnected s ↔ (∃ t, IsConnected t ∧ s = Sum.inl '' t) ∨ ∃ t, IsConnected t ∧ s = Sum.inr '' t :=
by
refine ⟨fun hs => ?_, ?_⟩
· obtain ⟨x | x, hx⟩ := hs.nonempty
· have h : s ⊆ range Sum.inl := hs.isPreconnected.subset_isClopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩
refine Or.inl ⟨Sum.inl ⁻¹' s, ?_, ?_⟩
· exact hs.preimage_of_isOpenMap Sum.inl_injective isOpenMap_inl h
· exact (image_preimage_eq_of_subset h).symm
· have h : s ⊆ range Sum.inr := hs.isPreconnected.subset_isClopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
refine Or.inr ⟨Sum.inr ⁻¹' s, ?_, ?_⟩
· exact hs.preimage_of_isOpenMap Sum.inr_injective isOpenMap_inr h
· exact (image_preimage_eq_of_subset h).symm
· rintro (⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩)
· exact ht.image _ continuous_inl.continuousOn
· exact ht.image _ continuous_inr.continuousOn
