mem_innerDualCone — Mathlib

English

Membership in innerDualCone is equivalent to the standard inner-product criterion.

Русский

Принадлежность innerDualCone эквивалентна стандартному критерию по скалярному произведению.

LaTeX

$$$y\\in s.innerDualCone\\iff \\forall x\\in s,\\ \\langle x,y\\rangle\\ge 0$$$

Lean4

@[deprecated ProperCone.mem_innerDual (since := "2025-07-06")]
theorem mem_innerDualCone (y : H) (s : Set H) : y ∈ s.innerDualCone ↔ ∀ x ∈ s, 0 ≤ ⟪x, y⟫ :=
  Iff.rfl

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