mathlib

653fe45e - feat(analysis/seminorm): `semilattice_sup` on seminorms and lemmas about `ball` (#11329)

feat(analysis/seminorm): `semilattice_sup` on seminorms and lemmas about `ball` (#11329) Define `bot` and the the binary `sup` on seminorms, and some lemmas about the supremum of a finite number of seminorms. Shows that the unit ball of the supremum is given by the intersection of the unit balls. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>