Commit 2022-01-26 13:29 590b5eb4

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