positive

Mathlib.Analysis.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#ProperCone.positive

← MathLib Explorer

English

The image of a cone under the identity map equals the cone itself.

Русский

Образ конуса под тождественным отображением равен самому конусу.

LaTeX

$$C.map( id ) = C$$

Lean4

/-- The positive cone is the proper cone formed by the set of nonnegative elements in an ordered
module. -/
@[simps!]
def positive : ProperCone R E where
  toSubmodule := PointedCone.positive R E
  isClosed' := isClosed_Ici

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru