span — Mathlib

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

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