mem_positive

Mathlib.Geometry.Convex.Cone.Basic

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

English

An element x lies in the positive cone if and only if x is nonnegative: x ∈ positive(R,M) ⇔ 0 ≤ x.

Русский

Элемент x принадлежит положительному конусу тогда и только тогда, когда x неотрицательно: x ∈ positive(R,M) ⇔ 0 ≤ x.

LaTeX

$$x \\in positive(R,M) \\iff 0 \\le x$$

Lean4

@[simp]
theorem mem_positive : x ∈ positive R M ↔ 0 ≤ x :=
  .rfl

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

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

Разделы

Аффилиация

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