English
The strictly positive cone is blunt
Русский
Строго положительный конус является blunt
LaTeX
$$Blunt(strictlyPositive(R,M))$$
Lean4
/-- The set of vectors proportional to those in a convex set forms a convex cone. -/
def toCone (s : Set M) (hs : Convex 𝕜 s) : ConvexCone 𝕜 M :=
by
apply ConvexCone.mk (⋃ (c : 𝕜) (_ : 0 < c), c • s) <;> simp only [mem_iUnion, mem_smul_set]
· rintro c c_pos _ ⟨c', c'_pos, x, hx, rfl⟩
exact ⟨c * c', mul_pos c_pos c'_pos, x, hx, (smul_smul _ _ _).symm⟩
· rintro _ ⟨cx, cx_pos, x, hx, rfl⟩ _ ⟨cy, cy_pos, y, hy, rfl⟩
have : 0 < cx + cy := add_pos cx_pos cy_pos
refine ⟨_, this, _, convex_iff_div.1 hs hx hy cx_pos.le cy_pos.le this, ?_⟩
simp only [smul_add, smul_smul, mul_div_assoc', mul_div_cancel_left₀ _ this.ne']
