how to prove the convex here.

Stream: mathlib4

[Katherine Wei]

theorem K_polar_convex: Convex ℝ (K_polar vmatrix) := by
  rw[Convex]
  intro x hx
  rw[K_polar] at hx
  simp at hx

⊢ StarConvex ℝ x (K_polar vmatrix)

[Ruben Van de Velde]

Kinda hard to say without knowing what K_polar is

[Katherine Wei]

def K_polar: Set (Fin n → ℝ) :=
{y | ∀ x ∈ K vmatrix, y ⬝ᵥ x ≤ 0}

[Kim Morrison]

(Posting questions as an #mwe makes it much more likely to get a good answer!)