positive — Mathlib

English

The positive cone is the cone of nonnegative elements in an ordered module, i.e., the set { x ∈ E | 0 ≤ x }. It forms a pointed cone.

Русский

Положительный конус — это конус неотрицательных элементов в упорядоченном модуле, то есть { x ∈ E | 0 ≤ x }. Это образует направленный конус.

LaTeX

$$$\text{positive}(R,E) = \{ x \in E \mid 0 \le x \}$$$

Lean4

/-- The positive cone is the pointed cone formed by the set of nonnegative elements in an ordered
module. -/
def positive : PointedCone R E :=
  (ConvexCone.positive R E).toPointedCone ConvexCone.pointed_positive

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