toConvexCone — Mathlib

English

Every submodule C of M is naturally a convex cone, with carrier C, closed under scalar multiplication and addition.

Русский

Каждый подмодуль C пространства M естественным образом является выпуклым конусом: носитель — C, замкнут относительно умножения на скаляры и сложения.

LaTeX

$$toConvexCone(C) = ConvexCone with carrier C.$$

Lean4

/-- Every submodule is trivially a convex cone. -/
def toConvexCone (C : Submodule R M) : ConvexCone R M
    where
  carrier := C
  smul_mem' c _ _ hx := C.smul_mem c hx
  add_mem' _ hx _ hy := C.add_mem hx hy

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