mathlib

590b5eb4 - feat(analysis/seminorm): The norm as a seminorm, balanced and absorbent lemmas (#11487)

feat(analysis/seminorm): The norm as a seminorm, balanced and absorbent lemmas (#11487) This * defines `norm_seminorm`, the norm as a seminorm. This is useful to translate seminorm lemmas to norm lemmas * proves many lemmas about `balanced`, `absorbs`, `absorbent` * generalizes many lemmas about the aforementioned predicates. In particular, `one_le_gauge_of_not_mem` now takes `(star_convex ℝ 0 s) (absorbs ℝ s {x})` instead of `(convex ℝ s) ((0 : E) ∈ s) (is_open s)`. The new `star_convex` lemmas justify that it's a generalization. * proves `star_convex_zero_iff` * proves `ne_zero_of_norm_ne_zero` and friends * makes `x` implicit in `convex.star_convex` * renames `balanced.univ` to `balanced_univ`