…ointwise operations (#17253)

Provides `sInter` and `sUnion` versions of  pointwise algebraic operations on sets.

Needed in #17029



Co-authored-by: Christopher Hoskin <[email protected]>

…Hull (#17029)

Defines the absolutely convex (or disked) hull of a subset of a locally convex space and proves a number of standard properties, including:

-  (subject to suitable conditions) the absolutely convex hull equals the convex hull of the balanced hull.
- In a real vector space the absolutely convex hull of `s` equals the convex hull of `s ∪ -s`



Co-authored-by: Christopher Hoskin <[email protected]>

… a single ring of scalars (#29342)

Currently the definition of Absolutely Convex in Mathlib is a little unexpected:
```
def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s
```
At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't  have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`.

Recently the requirements for the definition of `Convex` have been relaxed (#24392, #20595) so it is now possible to use a single scalar ring in common with the literature.

Previous discussion:

- #17029 (comment)
- #26345 (comment)

… a single ring of scalars (leanprover-community#29342)

Currently the definition of Absolutely Convex in Mathlib is a little unexpected:
```
def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s
```
At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't  have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`.

Recently the requirements for the definition of `Convex` have been relaxed (leanprover-community#24392, leanprover-community#20595) so it is now possible to use a single scalar ring in common with the literature.

Previous discussion:

- leanprover-community#17029 (comment)
- leanprover-community#26345 (comment)

… a single ring of scalars (leanprover-community#29342)

Currently the definition of Absolutely Convex in Mathlib is a little unexpected:
```
def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s
```
At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't  have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`.

Recently the requirements for the definition of `Convex` have been relaxed (leanprover-community#24392, leanprover-community#20595) so it is now possible to use a single scalar ring in common with the literature.

Previous discussion:

- leanprover-community#17029 (comment)
- leanprover-community#26345 (comment)