feat(analysis/seminorm): define the Minkowski functional (#9097)

This defines the gauge of a set, aka the Minkowski functional, in a vector space over a real normed field.

Co-authored-by: <bhavikmehta8@gmail.com>