Defining proper (convex) cones

Stream: maths

[Apurva Nakade]

I'm working on proving some geometric theorems about convex cones here #15637. I now have a few theorems that only hold true for convex cones that are closed and nonempty.

lemma pointed_of_nonempty_closed
  {K : convex_cone ℝ H} (ne : (K : set H).nonempty) (hc : is_closed (K : set H)) :
  K.pointed := sorry

theorem geometric_farkas_lemma
  {K : convex_cone ℝ H} (ne : (K : set H).nonempty) (hc : is_closed (K : set H))
  {b : H} (disj : b ∉ K) :
  ∃ (y : H), (∀ x : H, x ∈ K → 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0 := sorry

theorem dual_of_dual_eq_self
  {K : convex_cone ℝ H} (ne : (K : set H).nonempty) (hc : is_closed (K : set H)) :
  ((K : set H).inner_dual_cone : set H).inner_dual_cone = K := sorry

Should I define a new structure called proper_cone (= closed, nonempty, convex cone), create some basic API, and phrase the above results only for proper cones? The last result allows us to define an involutive star operation on proper cones which suggests that this is the correct definition.

These are the only cones used in the definition of a conic program so I can refactor this definition into a conic programming file later once I have a few basic results about it.