mathlib

e4a1e80f - feat(analysis/convex/combination): Convex hull of a `set.prod` and `set.pi` (#10125)

feat(analysis/convex/combination): Convex hull of a `set.prod` and `set.pi` (#10125) This proves * `(∀ i, convex 𝕜 (t i)) → convex 𝕜 (s.pi t)` * `convex_hull 𝕜 (s.prod t) = (convex_hull 𝕜 s).prod (convex_hull 𝕜 t)` * `convex_hull 𝕜 (s.pi t) = s.pi (convex_hull 𝕜 ∘ t)`