mathlib3

6bb17284 - feat(analysis/convex): interiors/closures of convex sets are convex in a tvs (#1781)

feat(analysis/convex): interiors/closures of convex sets are convex in a tvs (#1781) * feat(topology/algebra/module): scalar multiplication homeomorphisms * feat(topology/algebra/module): more lemmas - homeomorphisms given by scalar multiplication by unit is open/closed map. * feat(analysis/convex): interior of convex set is convex in a tvs - in separate file for interpretation time reasons. * feat(analysis/convex): extract lemma * feat(analysis/convex): closure of a convext set is convex * style(analysis/convex): place lemmas at reasonable locations * style(topology/algebra/module): fix bracketing style * feat(analysis/convex): introduce `smul_set` and `pointwise_mul` - also additional equivalent statements for convexity using those definitions. * feat(algebra/pointwise): lemmas for `smul_set` * doc(algebra/pointwise): add docstrings * doc(algebra/pointwise): add global docstring * docs(algebra/pointwise): amend global docstring