dual_dual — Mathlib

English

For a proper cone K, the dual of the dual of K (viewed as a convex cone) equals K. Dual of Dual equals original cone.

Русский

Для правильного конуса K двойной конус (через двойственную операцию) возвращает исходный конус.

LaTeX

$$$ (K.innerDualCone).innerDualCone = K $$$

Lean4

/-- The dual of the dual of a proper cone is itself. -/
@[deprecated ProperCone.innerDual_innerDual (since := "2025-07-06")]
theorem dual_dual (K : ProperCone ℝ H) : innerDual (innerDual (K : Set H)) = K :=
  ProperCone.toPointedCone_injective <|
    PointedCone.toConvexCone_injective <|
      (K : ConvexCone ℝ H).innerDualCone_of_innerDualCone_eq_self K.nonempty K.isClosed

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