English
If topological space E has a topology generated by a countable family p of seminorms, then E is first-countable.
Русский
Если топология пространства E задаётся счётным семейством семинорм, то пространство является первого счётного рода.
LaTeX
$$$ WithSeminorms p \\Rightarrow FirstCountableTopology E $$$
Lean4
/-- If the topology of a space is induced by a countable family of seminorms, then the topology
is first countable. -/
theorem firstCountableTopology (hp : WithSeminorms p) : FirstCountableTopology E :=
by
have := hp.topologicalAddGroup
let _ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
have : (𝓝 (0 : E)).IsCountablyGenerated :=
by
rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]
exact Filter.iInf.isCountablyGenerated _
have : (uniformity E).IsCountablyGenerated := IsUniformAddGroup.uniformity_countably_generated
exact UniformSpace.firstCountableTopology E
