𝕜 : Type u_1
𝕜₂ : Type ?u.182411
𝕝 : Type ?u.182414
𝕝₂ : Type ?u.182417
E : Type u_2
F : Type ?u.182423
G : Type ?u.182426
ι : Type u_3
ι' : Type ?u.182432
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ Filter.HasBasis (𝓝 0) (fun s => s ∈ SeminormFamily.basisSets p) id
𝕜 : Type u_1
𝕜₂ : Type ?u.182411
𝕝 : Type ?u.182414
𝕝₂ : Type ?u.182417
E : Type u_2
F : Type ?u.182423
G : Type ?u.182426
ι : Type u_3
ι' : Type ?u.182432
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ Filter.HasBasis (𝓝 0) (fun s => s ∈ SeminormFamily.basisSets p) id
rw [congr_fun (congr_arg (@nhds E) hp.1) 0]
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.182411
𝕝 : Type ?u.182414
𝕝₂ : Type ?u.182417
E : Type u_2
F : Type ?u.182423
G : Type ?u.182426
ι : Type u_3
ι' : Type ?u.182432
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ Filter.HasBasis (𝓝 0) (fun s => s ∈ SeminormFamily.basisSets p) id
exact AddGroupFilterBasis.nhds_zero_hasBasis _