α : Type u
β : Type v
ι : Type ?u.114625
π : ι → Type ?u.114630
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen (connectedComponentIn univ x)
α : Type u
β : Type v
ι : Type ?u.114625
π : ι → Type ?u.114630
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen (connectedComponent x)
rw [← connectedComponentIn_univ]
no goals
α : Type u
β : Type v
ι : Type ?u.114625
π : ι → Type ?u.114630
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
x : α
⊢ IsOpen (connectedComponentIn univ x)
exact isOpen_univ.connectedComponentIn