mathlib3

05213440 - feat(analysis/locally_convex/basic): add lemmas about finite unions for absorbs (#13236)

feat(analysis/locally_convex/basic): add lemmas about finite unions for absorbs (#13236) - Lemma for absorbing sets and addition - Two Lemmas for absorbing sets as finite unions (set.finite and finset variant) - Lemma for absorbent sets absorb finite sets. Co-authored-by: Moritz Doll <doll@uni-bremen.de>