PointedCone — Mathlib

English

A pointed cone is a submodule of a module where the scalars are restricted to nonnegative elements of the base ring.

Русский

Заострённый конус есть подподмодуль модуля над кольцом, где скаляры берутся из подполе неотрицательных элементов: { c ∈ R | 0 ≤ c }.

LaTeX

$$$\mathrm{PointedCone}(R,E) = \mathrm{Submodule}_{\{ c \in R \mid 0 \le c \}} E$$$

Lean4

/-- A pointed cone is a submodule of a module with scalars restricted to being nonnegative. -/
abbrev PointedCone (R E) [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] :=
  Submodule { c : R // 0 ≤ c } E

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