feat(analysis/seminorm): add inf (#11791)
Define the infimum of seminorms.
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: pbazin <75327486+pbazin@users.noreply.github.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
