feat(Analysis/Convex/Cone/Proper): define ProperCone.positive extendi…

…ng ConvexCone.positive (#6059)

Defines `ProperCone.positive` extending `ConvexCone.positive`.

Part of #6058

Mathlib/Analysis/Convex/Cone/Proper.lean

@@ -21,7 +21,6 @@ linear programs, the results from this file can be used to prove duality theorem
 
 The next steps are:
 - Add convex_cone_class that extends set_like and replace the below instance
-- Define the positive cone as a proper cone.
 - Define primal and dual cone programs and prove weak duality.
 - Prove regular and strong duality for cone programs using Farkas' lemma (see reference).
 - Define linear programs and prove LP duality as a special case of cone duality.
@@ -125,6 +124,29 @@ protected theorem isClosed (K : ProperCone 𝕜 E) : IsClosed (K : Set E) :=
 
 end SMul
 
+section PositiveCone
+
+variable (𝕜 E) 
+variable [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E]
+  [TopologicalSpace E] [OrderClosedTopology E]
+
+/-- The positive cone is the proper cone formed by the set of nonnegative elements in an ordered
+module. -/
+def positive : ProperCone 𝕜 E where
+  toConvexCone := ConvexCone.positive 𝕜 E
+  nonempty' := ⟨0, ConvexCone.pointed_positive _ _⟩
+  is_closed' := isClosed_Ici
+
+@[simp]
+theorem mem_positive {x : E} : x ∈ positive 𝕜 E ↔ 0 ≤ x :=
+  Iff.rfl
+
+@[simp]
+theorem coe_positive : ↑(positive 𝕜 E) = ConvexCone.positive 𝕜 E :=
+  rfl
+
+end PositiveCone
+
 section Module
 
 variable {𝕜 : Type _} [OrderedSemiring 𝕜]