Commit 2021-11-08 11:43 e4a1e80f
View on Github →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)