toConvexCone — Mathlib

English

Every pointed cone can be regarded as a convex cone.

Русский

Каждый заострённый конус можно рассматривать как выпуклый конус.

LaTeX

$$$\mathrm{toConvexCone}(C) \text{ is a convex cone with carrier } C$$$

Lean4

/-- Every pointed cone is a convex cone. -/
@[coe]
def toConvexCone (C : PointedCone R E) : ConvexCone R E
    where
  carrier := C
  smul_mem' c hc _ hx := C.smul_mem ⟨c, le_of_lt hc⟩ hx
  add_mem' _ hx _ hy := C.add_mem hx hy

Похожие утверждения