𝕜 : Type u_1
𝕜₂ : Type ?u.446340
𝕝 : Type ?u.446343
𝕝₂ : Type ?u.446346
E : Type u_2
F : Type ?u.446352
G : Type ?u.446355
ι : Type u_3
ι' : Type ?u.446361
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (𝓝 0 = ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)) ↔ 𝓝 0 = ⨅ (i : ι), 𝓝 0
𝕜 : Type u_1
𝕜₂ : Type ?u.446340
𝕝 : Type ?u.446343
𝕝₂ : Type ?u.446346
E : Type u_2
F : Type ?u.446352
G : Type ?u.446355
ι : Type u_3
ι' : Type ?u.446361
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ t = ⨅ (i : ι), UniformSpace.toTopologicalSpace
rw [p.withSeminorms_iff_nhds_eq_iInf,
  TopologicalAddGroup.ext_iff inferInstance (topologicalAddGroup_iInf fun i => inferInstance),
  nhds_iInf]
𝕜 : Type u_1
𝕜₂ : Type ?u.446340
𝕝 : Type ?u.446343
𝕝₂ : Type ?u.446346
E : Type u_2
F : Type ?u.446352
G : Type ?u.446355
ι : Type u_3
ι' : Type ?u.446361
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (𝓝 0 = ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)) = (𝓝 0 = ⨅ (i : ι), 𝓝 0)
𝕜 : Type u_1
𝕜₂ : Type ?u.446340
𝕝 : Type ?u.446343
𝕝₂ : Type ?u.446346
E : Type u_2
F : Type ?u.446352
G : Type ?u.446355
ι : Type u_3
ι' : Type ?u.446361
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (𝓝 0 = ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)) ↔ 𝓝 0 = ⨅ (i : ι), 𝓝 0
refine Eq.to_iff ?_
case e_a.e_s
𝕜 : Type u_1
𝕜₂ : Type ?u.446340
𝕝 : Type ?u.446343
𝕝₂ : Type ?u.446346
E : Type u_2
F : Type ?u.446352
G : Type ?u.446355
ι : Type u_3
ι' : Type ?u.446361
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (fun i => Filter.comap (↑(p i)) (𝓝 0)) = fun i => 𝓝 0
𝕜 : Type u_1
𝕜₂ : Type ?u.446340
𝕝 : Type ?u.446343
𝕝₂ : Type ?u.446346
E : Type u_2
F : Type ?u.446352
G : Type ?u.446355
ι : Type u_3
ι' : Type ?u.446361
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (𝓝 0 = ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)) = (𝓝 0 = ⨅ (i : ι), 𝓝 0)
congr
case e_a.e_s.h
𝕜 : Type u_1
𝕜₂ : Type ?u.446340
𝕝 : Type ?u.446343
𝕝₂ : Type ?u.446346
E : Type u_2
F : Type ?u.446352
G : Type ?u.446355
ι : Type u_3
ι' : Type ?u.446361
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ Filter.comap (↑(p i)) (𝓝 0) = 𝓝 0
case e_a.e_s
𝕜 : Type u_1
𝕜₂ : Type ?u.446340
𝕝 : Type ?u.446343
𝕝₂ : Type ?u.446346
E : Type u_2
F : Type ?u.446352
G : Type ?u.446355
ι : Type u_3
ι' : Type ?u.446361
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (fun i => Filter.comap (↑(p i)) (𝓝 0)) = fun i => 𝓝 0
funext i
no goals
case e_a.e_s.h
𝕜 : Type u_1
𝕜₂ : Type ?u.446340
𝕝 : Type ?u.446343
𝕝₂ : Type ?u.446346
E : Type u_2
F : Type ?u.446352
G : Type ?u.446355
ι : Type u_3
ι' : Type ?u.446361
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ Filter.comap (↑(p i)) (𝓝 0) = 𝓝 0
exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup