case intro
α : Type u
β : Type v
ι : Type ?u.4449
π : ι → Type ?u.4454
inst✝ : TopologicalSpace α
s✝ t✝ u v s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsConnected (s ∪ t)
α : Type u
β : Type v
ι : Type ?u.4449
π : ι → Type ?u.4454
inst✝ : TopologicalSpace α
s✝ t✝ u v s t : Set α
H : Set.Nonempty (s ∩ t)
Hs : IsConnected s
Ht : IsConnected t
⊢ IsConnected (s ∪ t)
rcases H with ⟨x, hx⟩
case intro
α : Type u
β : Type v
ι : Type ?u.4449
π : ι → Type ?u.4454
inst✝ : TopologicalSpace α
s✝ t✝ u v s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsPreconnected (s ∪ t)
case intro
α : Type u
β : Type v
ι : Type ?u.4449
π : ι → Type ?u.4454
inst✝ : TopologicalSpace α
s✝ t✝ u v s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsConnected (s ∪ t)
refine' ⟨⟨x, mem_union_left t (mem_of_mem_inter_left hx)⟩, _⟩
no goals
case intro
α : Type u
β : Type v
ι : Type ?u.4449
π : ι → Type ?u.4454
inst✝ : TopologicalSpace α
s✝ t✝ u v s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsPreconnected (s ∪ t)
exact Hs.isPreconnected.union x (mem_of_mem_inter_left hx) (mem_of_mem_inter_right hx)
  Ht.isPreconnected