mathlib

0da54467 - refactor(analysis/convex/basic): Redefine convexity in terms of star-convexity (#16173)

refactor(analysis/convex/basic): Redefine convexity in terms of star-convexity (#16173) Change the definition from ```lean def convex : Prop := ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s ``` to ```lean def convex : Prop := ∀ ⦃x : E⦄, x ∈ s → star_convex 𝕜 x s ``` which is defeq up to swapping the second and third foralls. This allows golfing the `convex` API in terms of the `star_convex` one. Also generalize `convex_pi` by limiting quantification to the set.