with_seminorms): fix namespaces for dot-notation (#16771)

Commit

3 years ago

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

Author

mcdoll

Parents