Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-03 06:36 d2461773

View on Github →

chore(analysis/locally_convex/with_seminorms): fix namespaces for dot-notation (#16771) Some lemmas where in the wrong namespaces.

Estimated changes

Modified src/analysis/locally_convex/weak_dual.lean

Modified src/analysis/locally_convex/with_seminorms.lean

deleted theorem seminorm_family.to_locally_convex_space

deleted theorem seminorm_family.with_seminorms_eq

added theorem with_seminorms.to_locally_convex_space

added theorem with_seminorms.with_seminorms_eq

Modified src/analysis/schwartz_space.lean