case mp
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ LocallyConnectedSpace α → ∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)

case mpr
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)) → LocallyConnectedSpace α
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ LocallyConnectedSpace α ↔ ∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)
constructor
case mp
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
h : LocallyConnectedSpace α
⊢ ∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)
case mp
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ LocallyConnectedSpace α → ∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)
intro h
no goals
case mp
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
h : LocallyConnectedSpace α
⊢ ∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)
exact fun F hF x _ => hF.connectedComponentIn
case mpr
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)
⊢ LocallyConnectedSpace α
case mpr
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)) → LocallyConnectedSpace α
intro h
case mpr
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)
⊢ ∀ (x : α) (U : Set α), U ∈ 𝓝 x → ∃ V, V ⊆ U ∧ IsOpen V ∧ x ∈ V ∧ IsConnected V
case mpr
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)
⊢ LocallyConnectedSpace α
rw [locallyConnectedSpace_iff_open_connected_subsets]
no goals
case mpr
α : Type u
β : Type v
ι : Type ?u.115042
π : ι → Type ?u.115047
inst✝ : TopologicalSpace α
s t u v : Set α
h : ∀ (F : Set α), IsOpen F → ∀ (x : α), x ∈ F → IsOpen (connectedComponentIn F x)
⊢ ∀ (x : α) (U : Set α), U ∈ 𝓝 x → ∃ V, V ⊆ U ∧ IsOpen V ∧ x ∈ V ∧ IsConnected V
refine' fun x U hU =>
    ⟨connectedComponentIn (interior U) x,
      (connectedComponentIn_subset _ _).trans interior_subset, h _ isOpen_interior x _,
      mem_connectedComponentIn _, isConnected_connectedComponentIn_iff.mpr _⟩ <;>
  exact mem_interior_iff_mem_nhds.mpr hU