α : Type u
β : Type v
ι : Type ?u.116595
π : ι → Type ?u.116600
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∀ (x : α) (U : Set α), U ∈ 𝓝 x → ∃ V, V ∈ 𝓝 x ∧ IsPreconnected V ∧ V ⊆ U) ↔
    ∀ (x : α), Filter.HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id
α : Type u
β : Type v
ι : Type ?u.116595
π : ι → Type ?u.116600
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), Filter.HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id
rw [locallyConnectedSpace_iff_connected_subsets]
no goals
α : Type u
β : Type v
ι : Type ?u.116595
π : ι → Type ?u.116600
inst✝ : TopologicalSpace α
s t u v : Set α
⊢ (∀ (x : α) (U : Set α), U ∈ 𝓝 x → ∃ V, V ∈ 𝓝 x ∧ IsPreconnected V ∧ V ⊆ U) ↔
    ∀ (x : α), Filter.HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id
exact forall_congr' <| fun x => Filter.hasBasis_self.symm