mem_dual

Mathlib.Geometry.Convex.Cone.Dual

URI: https://scilib.ai/kg/mathlib#PointedCone.mem_dual

English

The dual cone with respect to a bilinear form p is the set of all y such that p(x,y) ≥ 0 for all x ∈ s.

Русский

Двойственный конус к s состоит из таких y, что p(x,y) ≥ 0 для всех x ∈ s.

LaTeX

$$y ∈ dual p s ↔ ∀ x ∈ s, 0 ≤ p x y$$

Lean4

@[simp]
theorem mem_dual : y ∈ dual p s ↔ ∀ ⦃x⦄, x ∈ s → 0 ≤ p x y :=
  .rfl

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

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

Разделы

Аффилиация

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