innerDual — Mathlib

English

For a set s in E, the dual cone innerDual(s) consists of all y in E such that ⟪x,y⟫ ≥ 0 for every x ∈ s.

Русский

Для множества s в E двойной конус innerDual(s) состоит из всех y в E таких, что ⟪x,y⟫ ≥ 0 для всякого x ∈ s.

LaTeX

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

Lean4

/-- The dual cone of a set `s` is the cone consisting of all points `y` such that for all points
`x ∈ s` we have `0 ≤ ⟪x, y⟫`. -/
@[simps! toSubmodule]
def innerDual (s : Set E) : ProperCone ℝ E :=
  .dual (innerₗ E) s

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