α : Type u
β : Type v
ι : Type ?u.113849
π : ι → Type ?u.113854
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
h : ∃ i, (IsOpen i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F
⊢ connectedComponentIn F x ∈ 𝓝 x
α : Type u
β : Type v
ι : Type ?u.113849
π : ι → Type ?u.113854
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
h : F ∈ 𝓝 x
⊢ connectedComponentIn F x ∈ 𝓝 x
rw [(LocallyConnectedSpace.open_connected_basis x).mem_iff] at h
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.113849
π : ι → Type ?u.113854
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
s : Set α
hsF : id s ⊆ F
h1s : IsOpen s
hxs : x ∈ s
h2s : IsConnected s
⊢ connectedComponentIn F x ∈ 𝓝 x
α : Type u
β : Type v
ι : Type ?u.113849
π : ι → Type ?u.113854
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
h : ∃ i, (IsOpen i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F
⊢ connectedComponentIn F x ∈ 𝓝 x
rcases h with ⟨s, ⟨h1s, hxs, h2s⟩, hsF⟩
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.113849
π : ι → Type ?u.113854
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
s : Set α
hsF : id s ⊆ F
h1s : IsOpen s
hxs : x ∈ s
h2s : IsConnected s
⊢ connectedComponentIn F x ∈ 𝓝 x
exact mem_nhds_iff.mpr ⟨s, h2s.isPreconnected.subset_connectedComponentIn hxs hsF, h1s, hxs⟩