mathlib

49cd1cc6 - refactor(analysis/seminorm): move topology induced by seminorms to its own file (#12826)

refactor(analysis/seminorm): move topology induced by seminorms to its own file (#12826) Besides the copy and paste I removed the namespace `seminorm` from most parts (it is still there for the boundedness definitions and statements) and updated the module docstrings. No real code has changed.