English
Let α and β be topological spaces. For any subset s of the disjoint sum α ⊕ β, s is preconnected if and only if s lies entirely in one of the two summands; more precisely, there exists a set t ⊆ α which is preconnected and s = inl''t, or there exists a set t ⊆ β which is preconnected and s = inr''t.
Русский
Пусть α и β — топологические пространства. Для любой подмножества s из дизъюнкции α ⊕ β, предсвязанность s эквивалентна тому, что s лежит целиком в одной из компонент: существует предсвязанное множество t ⊆ α с s = inl''t, или существует предсвязанное множество t ⊆ β с s = inr''t.
LaTeX
$$$\text{IsPreconnected}(s) \iff \Big(\exists t\, (IsPreconnected(t) \land s = \mathrm{Sum.inl}''t) \Big) \lor \Big(\exists t\, (IsPreconnected(t) \land s = \mathrm{Sum.inr}''t)\Big)$$$
Lean4
theorem isPreconnected_iff [TopologicalSpace β] {s : Set (α ⊕ β)} :
IsPreconnected s ↔ (∃ t, IsPreconnected t ∧ s = Sum.inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = Sum.inr '' t :=
by
refine ⟨fun hs => ?_, ?_⟩
· obtain rfl | h := s.eq_empty_or_nonempty
· exact Or.inl ⟨∅, isPreconnected_empty, (Set.image_empty _).symm⟩
obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isConnected_iff.1 ⟨h, hs⟩
· exact Or.inl ⟨t, ht.isPreconnected, rfl⟩
· exact Or.inr ⟨t, ht.isPreconnected, rfl⟩
· rintro (⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩)
· exact ht.image _ continuous_inl.continuousOn
· exact ht.image _ continuous_inr.continuousOn
