𝕜 : Type u_1
𝕜₂ : Type ?u.438464
𝕝 : Type ?u.438467
𝕝₂ : Type ?u.438470
E : Type u_2
F : Type ?u.438476
G : Type ?u.438479
ι : Type u_3
ι' : Type ?u.438485
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
𝕜 : Type u_1
𝕜₂ : Type ?u.438464
𝕝 : Type ?u.438467
𝕝₂ : Type ?u.438470
E : Type u_2
F : Type ?u.438476
G : Type ?u.438479
ι : Type u_3
ι' : Type ?u.438485
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ 𝓝 0 = ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)
rw [← p.filter_eq_iInf]
𝕜 : Type u_1
𝕜₂ : Type ?u.438464
𝕝 : Type ?u.438467
𝕝₂ : Type ?u.438470
E : Type u_2
F : Type ?u.438476
G : Type ?u.438479
ι : Type u_3
ι' : Type ?u.438485
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
⊢ 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
𝕜 : Type u_1
𝕜₂ : Type ?u.438464
𝕝 : Type ?u.438467
𝕝₂ : Type ?u.438470
E : Type u_2
F : Type ?u.438476
G : Type ?u.438479
ι : Type u_3
ι' : Type ?u.438485
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
refine' ⟨fun h => _, p.withSeminorms_of_nhds⟩
𝕜 : Type u_1
𝕜₂ : Type ?u.438464
𝕝 : Type ?u.438467
𝕝₂ : Type ?u.438470
E : Type u_2
F : Type ?u.438476
G : Type ?u.438479
ι : Type u_3
ι' : Type ?u.438485
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
⊢ 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
𝕜 : Type u_1
𝕜₂ : Type ?u.438464
𝕝 : Type ?u.438467
𝕝₂ : Type ?u.438470
E : Type u_2
F : Type ?u.438476
G : Type ?u.438479
ι : Type u_3
ι' : Type ?u.438485
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
⊢ 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
rw [h.topology_eq_withSeminorms]
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.438464
𝕝 : Type ?u.438467
𝕝₂ : Type ?u.438470
E : Type u_2
F : Type ?u.438476
G : Type ?u.438479
ι : Type u_3
ι' : Type ?u.438485
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
⊢ 𝓝 0 = FilterBasis.filter AddGroupFilterBasis.toFilterBasis
exact AddGroupFilterBasis.nhds_zero_eq _