mathlib

d2bfb32b - feat(analysis/normed_space): range of `norm` (#14740)

feat(analysis/normed_space): range of `norm` (#14740) * Add `exists_norm_eq`, `range_norm`, `range_nnnorm`, and `nnnorm_surjective`. * Open `set` namespace.