Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-30 18:24 6e5e3f68

View on Github →

feat(analysis/locally_convex): the topology of a locally convex space is generated by seminorms (#15035) This PR provides the proof that every locally convex space has a family of seminorms that induces the topology. This PR also adds a new simp-lemma is_R_or_C.real_norm, which calculates the norm of a real number r coerced into a is_R_or_C type as the norm of r. This made it necessary to change some proofs in a few places.

Estimated changes

Modified src/analysis/complex/basic.lean

modified theorem complex.norm_real

Created src/analysis/locally_convex/abs_convex.lean

added theorem abs_convex_open_sets.coe_balanced

added theorem abs_convex_open_sets.coe_convex

added theorem abs_convex_open_sets.coe_is_open

added theorem abs_convex_open_sets.coe_nhds

added theorem abs_convex_open_sets.coe_zero_mem

added def abs_convex_open_sets

added def gauge_seminorm_family

added theorem gauge_seminorm_family_ball

added theorem nhds_basis_abs_convex

added theorem nhds_basis_abs_convex_open

added theorem with_gauge_seminorm_family

Modified src/analysis/locally_convex/basic.lean

added theorem balanced_convex_hull_of_balanced

Modified src/analysis/locally_convex/with_seminorms.lean

Modified src/analysis/normed_space/is_R_or_C.lean

modified theorem is_R_or_C.norm_coe_norm

Modified src/data/complex/is_R_or_C.lean

added theorem is_R_or_C.norm_real

deleted theorem is_R_or_C.norm_sq_of_real

Modified src/topology/algebra/module/locally_convex.lean