R : Type ?u.1410115
R' : Type ?u.1410118
𝕜 : Type ?u.1410121
𝕜₂ : Type ?u.1410124
𝕜₃ : Type ?u.1410127
𝕝 : Type u_2
E : Type u_1
E₂ : Type ?u.1410136
E₃ : Type ?u.1410139
F : Type ?u.1410142
G : Type ?u.1410145
ι : Type ?u.1410148
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedRing 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (↑p) 0
this : UniformSpace E := TopologicalAddGroup.toUniformSpace E
⊢ Continuous ↑p
R : Type ?u.1410115
R' : Type ?u.1410118
𝕜 : Type ?u.1410121
𝕜₂ : Type ?u.1410124
𝕜₃ : Type ?u.1410127
𝕝 : Type u_2
E : Type u_1
E₂ : Type ?u.1410136
E₃ : Type ?u.1410139
F : Type ?u.1410142
G : Type ?u.1410145
ι : Type ?u.1410148
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedRing 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (↑p) 0
⊢ Continuous ↑p
letI := TopologicalAddGroup.toUniformSpace E
R : Type ?u.1410115
R' : Type ?u.1410118
𝕜 : Type ?u.1410121
𝕜₂ : Type ?u.1410124
𝕜₃ : Type ?u.1410127
𝕝 : Type u_2
E : Type u_1
E₂ : Type ?u.1410136
E₃ : Type ?u.1410139
F : Type ?u.1410142
G : Type ?u.1410145
ι : Type ?u.1410148
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedRing 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (↑p) 0
this✝ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ Continuous ↑p
R : Type ?u.1410115
R' : Type ?u.1410118
𝕜 : Type ?u.1410121
𝕜₂ : Type ?u.1410124
𝕜₃ : Type ?u.1410127
𝕝 : Type u_2
E : Type u_1
E₂ : Type ?u.1410136
E₃ : Type ?u.1410139
F : Type ?u.1410142
G : Type ?u.1410145
ι : Type ?u.1410148
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedRing 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (↑p) 0
this : UniformSpace E := TopologicalAddGroup.toUniformSpace E
⊢ Continuous ↑p
haveI : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
no goals
R : Type ?u.1410115
R' : Type ?u.1410118
𝕜 : Type ?u.1410121
𝕜₂ : Type ?u.1410124
𝕜₃ : Type ?u.1410127
𝕝 : Type u_2
E : Type u_1
E₂ : Type ?u.1410136
E₃ : Type ?u.1410139
F : Type ?u.1410142
G : Type ?u.1410145
ι : Type ?u.1410148
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedRing 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (↑p) 0
this✝ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ Continuous ↑p
exact (Seminorm.uniformContinuous_of_continuousAt_zero hp).continuous