R : Type ?u.1398634
R' : Type ?u.1398637
𝕜 : Type ?u.1398640
𝕜₂ : Type ?u.1398643
𝕜₃ : Type ?u.1398646
𝕝 : Type u_2
E : Type u_1
E₂ : Type ?u.1398655
E₃ : Type ?u.1398658
F : Type ?u.1398661
G : Type ?u.1398664
ι : Type ?u.1398667
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedRing 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : Seminorm 𝕝 E
hp✝ : ContinuousAt (↑p) 0
hp : Filter.Tendsto (↑p) (𝓝 0) (𝓝 0)
⊢ UniformContinuous ↑p
R : Type ?u.1398634
R' : Type ?u.1398637
𝕜 : Type ?u.1398640
𝕜₂ : Type ?u.1398643
𝕜₃ : Type ?u.1398646
𝕝 : Type u_2
E : Type u_1
E₂ : Type ?u.1398655
E₃ : Type ?u.1398658
F : Type ?u.1398661
G : Type ?u.1398664
ι : Type ?u.1398667
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedRing 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (↑p) 0
⊢ UniformContinuous ↑p
have hp : Filter.Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp
R : Type ?u.1398634
R' : Type ?u.1398637
𝕜 : Type ?u.1398640
𝕜₂ : Type ?u.1398643
𝕜₃ : Type ?u.1398646
𝕝 : Type u_2
E : Type u_1
E₂ : Type ?u.1398655
E₃ : Type ?u.1398658
F : Type ?u.1398661
G : Type ?u.1398664
ι : Type ?u.1398667
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedRing 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : Seminorm 𝕝 E
hp✝ : ContinuousAt (↑p) 0
hp : Filter.Tendsto (↑p) (𝓝 0) (𝓝 0)
⊢ Filter.Tendsto ((fun p => dist p.fst p.snd) ∘ fun x => (↑p x.fst, ↑p x.snd))
    (Filter.comap (fun x => x.fst - x.snd) (𝓝 0)) (𝓝 0)
R : Type ?u.1398634
R' : Type ?u.1398637
𝕜 : Type ?u.1398640
𝕜₂ : Type ?u.1398643
𝕜₃ : Type ?u.1398646
𝕝 : Type u_2
E : Type u_1
E₂ : Type ?u.1398655
E₃ : Type ?u.1398658
F : Type ?u.1398661
G : Type ?u.1398664
ι : Type ?u.1398667
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedRing 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : Seminorm 𝕝 E
hp✝ : ContinuousAt (↑p) 0
hp : Filter.Tendsto (↑p) (𝓝 0) (𝓝 0)
⊢ UniformContinuous ↑p
rw [UniformContinuous, uniformity_eq_comap_nhds_zero_swapped,
  Metric.uniformity_eq_comap_nhds_zero, Filter.tendsto_comap_iff]
no goals
R : Type ?u.1398634
R' : Type ?u.1398637
𝕜 : Type ?u.1398640
𝕜₂ : Type ?u.1398643
𝕜₃ : Type ?u.1398646
𝕝 : Type u_2
E : Type u_1
E₂ : Type ?u.1398655
E₃ : Type ?u.1398658
F : Type ?u.1398661
G : Type ?u.1398664
ι : Type ?u.1398667
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedRing 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : Seminorm 𝕝 E
hp✝ : ContinuousAt (↑p) 0
hp : Filter.Tendsto (↑p) (𝓝 0) (𝓝 0)
⊢ Filter.Tendsto ((fun p => dist p.fst p.snd) ∘ fun x => (↑p x.fst, ↑p x.snd))
    (Filter.comap (fun x => x.fst - x.snd) (𝓝 0)) (𝓝 0)
exact
  tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hp.comp Filter.tendsto_comap)
    (fun xy => dist_nonneg) fun xy => p.norm_sub_map_le_sub _ _