mem_zero

Mathlib.Geometry.Convex.Cone.Basic

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

English

In the zero convex cone, x is a member iff x = 0.

Русский

В нулевом конусе элемент является членом тогда и только тогда, когда он равен нулю.

LaTeX

$$x ∈ (0 : ConvexCone R M) \iff x = 0$$

Lean4

@[simp]
theorem mem_zero : x ∈ (0 : ConvexCone R M) ↔ x = 0 :=
  .rfl

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

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

Разделы

Аффилиация

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