𝕜 : Type ?u.440749
𝕜₂ : Type ?u.440752
𝕝 : Type u_1
𝕝₂ : Type ?u.440758
E : Type u_2
F : Type ?u.440764
G : Type ?u.440767
ι : Type u_3
ι' : Type ?u.440773
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Nonempty ι
t : TopologicalSpace E
inst✝³ : TopologicalAddGroup E
inst✝² : NontriviallyNormedField 𝕝
inst✝¹ : Module 𝕝 E
inst✝ : ContinuousConstSMul 𝕝 E
p : SeminormFamily 𝕝 E ι
hp : WithSeminorms p
i : ι
⊢ ball (p i) 0 1 ∈ 𝓝 0
𝕜 : Type ?u.440749
𝕜₂ : Type ?u.440752
𝕝 : Type u_1
𝕝₂ : Type ?u.440758
E : Type u_2
F : Type ?u.440764
G : Type ?u.440767
ι : Type u_3
ι' : Type ?u.440773
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Nonempty ι
t : TopologicalSpace E
inst✝³ : TopologicalAddGroup E
inst✝² : NontriviallyNormedField 𝕝
inst✝¹ : Module 𝕝 E
inst✝ : ContinuousConstSMul 𝕝 E
p : SeminormFamily 𝕝 E ι
hp : WithSeminorms p
i : ι
⊢ Continuous ↑(p i)
refine' Seminorm.continuous one_pos _
𝕜 : Type ?u.440749
𝕜₂ : Type ?u.440752
𝕝 : Type u_1
𝕝₂ : Type ?u.440758
E : Type u_2
F : Type ?u.440764
G : Type ?u.440767
ι : Type u_3
ι' : Type ?u.440773
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Nonempty ι
t : TopologicalSpace E
inst✝³ : TopologicalAddGroup E
inst✝² : NontriviallyNormedField 𝕝
inst✝¹ : Module 𝕝 E
inst✝ : ContinuousConstSMul 𝕝 E
p : SeminormFamily 𝕝 E ι
hp : WithSeminorms p
i : ι
⊢ ↑(p i) ⁻¹' Metric.ball 0 1 ∈ ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)
𝕜 : Type ?u.440749
𝕜₂ : Type ?u.440752
𝕝 : Type u_1
𝕝₂ : Type ?u.440758
E : Type u_2
F : Type ?u.440764
G : Type ?u.440767
ι : Type u_3
ι' : Type ?u.440773
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Nonempty ι
t : TopologicalSpace E
inst✝³ : TopologicalAddGroup E
inst✝² : NontriviallyNormedField 𝕝
inst✝¹ : Module 𝕝 E
inst✝ : ContinuousConstSMul 𝕝 E
p : SeminormFamily 𝕝 E ι
hp : WithSeminorms p
i : ι
⊢ ball (p i) 0 1 ∈ 𝓝 0
rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp, ball_zero_eq_preimage_ball]
no goals
𝕜 : Type ?u.440749
𝕜₂ : Type ?u.440752
𝕝 : Type u_1
𝕝₂ : Type ?u.440758
E : Type u_2
F : Type ?u.440764
G : Type ?u.440767
ι : Type u_3
ι' : Type ?u.440773
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Nonempty ι
t : TopologicalSpace E
inst✝³ : TopologicalAddGroup E
inst✝² : NontriviallyNormedField 𝕝
inst✝¹ : Module 𝕝 E
inst✝ : ContinuousConstSMul 𝕝 E
p : SeminormFamily 𝕝 E ι
hp : WithSeminorms p
i : ι
⊢ ↑(p i) ⁻¹' Metric.ball 0 1 ∈ ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)
exact Filter.mem_iInf_of_mem i (Filter.preimage_mem_comap <| Metric.ball_mem_nhds _ one_pos)