innerDualCone_singleton — Mathlib

English

The dual cone of a singleton behaves as the preimage of the positive cone under the corresponding inner product map.

Русский

Двойной конус одиночного элемента ведёт себя как прообраз положительного конуса под соответствующим отображением скалярного произведения.

LaTeX

$$$\\text{innerDual}({x}) = \\text{comap}(\\text{inner}_{\\<·,•\\>}(x), \\text{positive})$$$

Lean4

/-- The inner dual cone of a singleton is given by the preimage of the positive cone under the
linear map `fun y ↦ ⟪x, y⟫`. -/
@[deprecated ProperCone.innerDual_singleton (since := "2025-07-06")]
theorem innerDualCone_singleton (x : H) :
    ({ x } : Set H).innerDualCone = (ConvexCone.positive ℝ ℝ).comap (innerₛₗ ℝ x) :=
  ConvexCone.ext fun _ => forall_eq

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