𝕜 : Type u_1
𝕜₂ : Type ?u.848749
𝕝 : Type ?u.848752
𝕝₂ : Type ?u.848755
E : Type u_2
F : Type ?u.848761
G : Type ?u.848764
ι : Type u_3
ι' : Type ?u.848770
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
hp : WithSeminorms p
this : Filter.IsCountablyGenerated (𝓝 0)
⊢ FirstCountableTopology E
𝕜 : Type u_1
𝕜₂ : Type ?u.848749
𝕝 : Type ?u.848752
𝕝₂ : Type ?u.848755
E : Type u_2
F : Type ?u.848761
G : Type ?u.848764
ι : Type u_3
ι' : Type ?u.848770
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
hp : WithSeminorms p
⊢ FirstCountableTopology E
have : (𝓝 (0 : E)).IsCountablyGenerated := by
  rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]
  exact Filter.iInf.isCountablyGenerated _
𝕜 : Type u_1
𝕜₂ : Type ?u.848749
𝕝 : Type ?u.848752
𝕝₂ : Type ?u.848755
E : Type u_2
F : Type ?u.848761
G : Type ?u.848764
ι : Type u_3
ι' : Type ?u.848770
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
hp : WithSeminorms p
this✝ : Filter.IsCountablyGenerated (𝓝 0)
this : Filter.IsCountablyGenerated (uniformity E)
⊢ FirstCountableTopology E
𝕜 : Type u_1
𝕜₂ : Type ?u.848749
𝕝 : Type ?u.848752
𝕝₂ : Type ?u.848755
E : Type u_2
F : Type ?u.848761
G : Type ?u.848764
ι : Type u_3
ι' : Type ?u.848770
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
hp : WithSeminorms p
this : Filter.IsCountablyGenerated (𝓝 0)
⊢ FirstCountableTopology E
haveI : (uniformity E).IsCountablyGenerated := UniformAddGroup.uniformity_countably_generated
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.848749
𝕝 : Type ?u.848752
𝕝₂ : Type ?u.848755
E : Type u_2
F : Type ?u.848761
G : Type ?u.848764
ι : Type u_3
ι' : Type ?u.848770
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
hp : WithSeminorms p
this✝ : Filter.IsCountablyGenerated (𝓝 0)
this : Filter.IsCountablyGenerated (uniformity E)
⊢ FirstCountableTopology E
exact UniformSpace.firstCountableTopology E
𝕜 : Type u_1
𝕜₂ : Type ?u.848749
𝕝 : Type ?u.848752
𝕝₂ : Type ?u.848755
E : Type u_2
F : Type ?u.848761
G : Type ?u.848764
ι : Type u_3
ι' : Type ?u.848770
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
hp : WithSeminorms p
⊢ Filter.IsCountablyGenerated (⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0))
𝕜 : Type u_1
𝕜₂ : Type ?u.848749
𝕝 : Type ?u.848752
𝕝₂ : Type ?u.848755
E : Type u_2
F : Type ?u.848761
G : Type ?u.848764
ι : Type u_3
ι' : Type ?u.848770
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
hp : WithSeminorms p
⊢ Filter.IsCountablyGenerated (𝓝 0)
rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.848749
𝕝 : Type ?u.848752
𝕝₂ : Type ?u.848755
E : Type u_2
F : Type ?u.848761
G : Type ?u.848764
ι : Type u_3
ι' : Type ?u.848770
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
hp : WithSeminorms p
⊢ Filter.IsCountablyGenerated (⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0))
exact Filter.iInf.isCountablyGenerated _