mathlib3

750f53c8 - feat(analysis/seminorm): define the topology induced by a family of seminorms (#11604)

feat(analysis/seminorm): define the topology induced by a family of seminorms (#11604) Define the topology induced by a single seminorm and by a family of seminorms and show that boundedness of linear maps implies continuity.