case intro.intro
α : Type u
β : Type v
ι : Type ?u.4171
π : ι → Type ?u.4176
inst✝ : TopologicalSpace α
s✝ t✝ u v s t : Set α
hs : IsPreconnected s
ht : IsPreconnected t
x : α
hxs : x ∈ s
hxt : x ∈ t
⊢ IsPreconnected (s ∪ t)
α : Type u
β : Type v
ι : Type ?u.4171
π : ι → Type ?u.4176
inst✝ : TopologicalSpace α
s✝ t✝ u v s t : Set α
H : Set.Nonempty (s ∩ t)
hs : IsPreconnected s
ht : IsPreconnected t
⊢ IsPreconnected (s ∪ t)
rcases H with ⟨x, hxs, hxt⟩
no goals
case intro.intro
α : Type u
β : Type v
ι : Type ?u.4171
π : ι → Type ?u.4176
inst✝ : TopologicalSpace α
s✝ t✝ u v s t : Set α
hs : IsPreconnected s
ht : IsPreconnected t
x : α
hxs : x ∈ s
hxt : x ∈ t
⊢ IsPreconnected (s ∪ t)
exact hs.union x hxs hxt ht