mem_innerDual — Mathlib

English

Membership in the dual cone of a set s is equivalent to the pointwise nonnegativity of the inner product with all elements of s.

Русский

Принадлежность к двойному конусу множества s эквивалентна неотрицательности скалярного произведения с любым элементом s.

LaTeX

$$$y\\in\\text{innerDual}(s)\\iff \\forall x\\in s,\\ \\langle x,y\\rangle\\ge 0$$$

Lean4

@[simp]
theorem mem_innerDual : y ∈ innerDual s ↔ ∀ ⦃x⦄, x ∈ s → 0 ≤ ⟪x, y⟫ :=
  .rfl

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