coe_strictlyPositive

Mathlib.Geometry.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#ConvexCone.coe_strictlyPositive

English

The strictly positive cone is salient, i.e., it does not contain nonzero elements along with their negatives.

Русский

Строго положительный конус является salient, то есть не содержит ненулевых элементов вместе с их отрицаниями.

LaTeX

$$Salient((strictlyPositive R M))$$

Lean4

@[simp]
theorem coe_strictlyPositive : ↑(strictlyPositive R M) = Set.Ioi (0 : M) :=
  rfl

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

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

Разделы

Аффилиация

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