α : Type u
β : Type v
ι : Type ?u.114324
π : ι → Type ?u.114329
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
⊢ ∀ (a : α), a ∈ connectedComponentIn F x → connectedComponentIn F x ∈ 𝓝 a
α : Type u
β : Type v
ι : Type ?u.114324
π : ι → Type ?u.114329
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
⊢ IsOpen (connectedComponentIn F x)
rw [isOpen_iff_mem_nhds]
α : Type u
β : Type v
ι : Type ?u.114324
π : ι → Type ?u.114329
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x ∈ 𝓝 y
α : Type u
β : Type v
ι : Type ?u.114324
π : ι → Type ?u.114329
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
⊢ ∀ (a : α), a ∈ connectedComponentIn F x → connectedComponentIn F x ∈ 𝓝 a
intro y hy
α : Type u
β : Type v
ι : Type ?u.114324
π : ι → Type ?u.114329
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F y ∈ 𝓝 y
α : Type u
β : Type v
ι : Type ?u.114324
π : ι → Type ?u.114329
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x ∈ 𝓝 y
rw [connectedComponentIn_eq hy]
no goals
α : Type u
β : Type v
ι : Type ?u.114324
π : ι → Type ?u.114329
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F y ∈ 𝓝 y
exact connectedComponentIn_mem_nhds (hF.mem_nhds <| connectedComponentIn_subset F x hy)