Theorems · Theorem · convex and discrete geometry

ProperCone.innerDual_singleton

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E] (x : E),
  ProperCone.innerDual {x} = ProperCone.comap ((innerSL ℝ) x) (ProperCone.positive ℝ ℝ)

The inner dual cone of a singleton is given by the preimage of the positive cone under the linear map fun y ↦ ⟪x, y⟫.

Defined in

Mathlib.Analysis.Convex.Cone.InnerDual

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceCompleteSpace