toConvexCone_dual — Mathlib

English

For a real pointed cone C that is a proper cone in H, the dual of C equals its inner dual cone: dual(inner)(C) = (C).innerDualCone.

Русский

Пусть C — правильный конус в вещественном пространстве H. Тогда двойственный конус C равен его внутреннему двойственному конусу.

LaTeX

$$$ dual (inner_\\ell H) C = (C : Set H).innerDualCone $$$

Lean4

@[deprecated "Now irrelevant" (since := "2025-07-06")]
theorem toConvexCone_dual (C : PointedCone ℝ H) :
    (dual (innerₗ H) (C : Set H)).toConvexCone = (C : Set H).innerDualCone :=
  rfl

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