Commit 2022-08-21 19:16 0da54467
View on Github →refactor(analysis/convex/basic): Redefine convexity in terms of star-convexity (#16173) Change the definition from
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
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.