English
The original set is contained in the span of itself as a pointed cone.
Русский
Любое множество содержится в span данного множества как pointed cone.
LaTeX
$$s ⊆ PointedCone.span R s$$
Lean4
/-- The span of a set `s` is the smallest pointed cone that contains `s`.
Pointed cones being defined as submodules over nonnegative scalars, this is exactly the
submodule span of `s` w.r.t. nonnegative scalars. -/
abbrev span (s : Set E) : PointedCone R E :=
Submodule.span R≥0 s