From 73d05c46b08a3db2c1b14cce11121daaa7552ded Mon Sep 17 00:00:00 2001 From: mcdoll Date: Sun, 2 Oct 2022 12:39:50 +0000 Subject: [PATCH] feat(analysis/locally_convex): first countable topologies from countable families of seminorms (#16595) This PR proves that if the topology is induced by a countable family of seminorms, then it is first countable. --- .../locally_convex/with_seminorms.lean | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean index 8f2a3de99edb4..065641be0c2bb 100644 --- a/src/analysis/locally_convex/with_seminorms.lean +++ b/src/analysis/locally_convex/with_seminorms.lean @@ -546,3 +546,23 @@ begin end end topological_constructions + +section topological_properties + +variables [nontrivially_normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι] [countable ι] +variables {p : seminorm_family 𝕜 E ι} +variables [uniform_space E] [uniform_add_group E] + +/-- If the topology of a space is induced by a countable family of seminorms, then the topology +is first countable. -/ +lemma with_seminorms.first_countable (hp : with_seminorms p) : + topological_space.first_countable_topology E := +begin + haveI : (𝓝 (0 : E)).is_countably_generated, + { rw p.with_seminorms_iff_nhds_eq_infi.mp hp, + exact filter.infi.is_countably_generated _ }, + haveI : (uniformity E).is_countably_generated := uniform_add_group.uniformity_countably_generated, + exact uniform_space.first_countable_topology E, +end + +end topological_properties