α : Type u
β : Type v
ι✝ : Type ?u.116895
π : ι✝ → Type ?u.116900
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_1
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), Filter.HasBasis (𝓝 x) (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ ∀ (x : α), Filter.HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id
α : Type u
β : Type v
ι✝ : Type ?u.116895
π : ι✝ → Type ?u.116900
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_1
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), Filter.HasBasis (𝓝 x) (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ LocallyConnectedSpace α
rw [locallyConnectedSpace_iff_connected_basis]
no goals
α : Type u
β : Type v
ι✝ : Type ?u.116895
π : ι✝ → Type ?u.116900
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_1
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), Filter.HasBasis (𝓝 x) (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ ∀ (x : α), Filter.HasBasis (𝓝 x) (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id
exact fun x =>
  (hbasis x).to_hasBasis
    (fun i hi => ⟨b x i, ⟨(hbasis x).mem_of_mem hi, hconnected x i hi⟩, subset_rfl⟩) fun s hs =>
    ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩