mathlib3

c46f021f - feat(analysis/seminorm): characterize continuity of seminorms by closed balls (#17249)