Commit 2024-02-03 07:19 4d359a9b

chore(Absorbs, Balanced): more lemmas, golf, generalize (#10201)

• add balanced_iff_closedBall_smul, balanced_neg;
• generalize Balanced.neg_mem_iff to a SeminormedRing + NormOneClass, add Balanced.neg_eq
• add Balanced.smul_mem_mono and Balanced.smul_congr;
• rename Balanced.mem_smul_iff to Balanced.smul_mem_iff;
• rename balanced_zero_union_interior to Balanced.zero_insert_interior, use insert 0 (interior A) instead of 0 ∪ interior A;
• make Balanced.interior and Balanced.closure protected;
• deprecate Absorbs.zero_mem';
• rename balanced_convexHull_of_balanced to Balanced.convexHull;
• add absorbs_iff_eventually_cobounded_mapsTo, use it to golf some proofs.