Theorems · Definition · convex and discrete geometry

ProperCone.innerDual

{E : Type u_2} →
  [inst : NormedAddCommGroup E] → [inst_1 : InnerProductSpace ℝ E] → [CompleteSpace E] → Set E → ProperCone ℝ E

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⟫.

Defined in

Mathlib.Analysis.Convex.Cone.InnerDual

Cited by

15 results in Mathlib

Foundations

Depth 185 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceCompleteSpace