𝕜 : Type u_1
𝕜₂ : Type ?u.180765
𝕝 : Type ?u.180768
𝕝₂ : Type ?u.180771
E : Type u_2
F : Type ?u.180777
G : Type ?u.180780
ι : Type u_3
ι' : Type ?u.180786
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ TopologicalAddGroup E
𝕜 : Type u_1
𝕜₂ : Type ?u.180765
𝕝 : Type ?u.180768
𝕝₂ : Type ?u.180771
E : Type u_2
F : Type ?u.180777
G : Type ?u.180780
ι : Type u_3
ι' : Type ?u.180786
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ TopologicalAddGroup E
rw [hp.withSeminorms_eq]
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.180765
𝕝 : Type ?u.180768
𝕝₂ : Type ?u.180771
E : Type u_2
F : Type ?u.180777
G : Type ?u.180780
ι : Type u_3
ι' : Type ?u.180786
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ TopologicalAddGroup E
exact AddGroupFilterBasis.isTopologicalAddGroup _