English
For a pointed cone C in a real inner product space H, the convex cone obtained from the dual equals the inner dual cone of C: toConvexCone(dual(C)) = C.innerDualCone.
Русский
Пусть C — направленный конус в вещественном пространстве с скалярным произведением. Двухразрядный конус (путь двойственного конуса) через двойственный образ равен внутреннему двойственному конусу C.
LaTeX
$$$ \\text{toConvexCone}(\\text{dual}(C)) = C.innerDualCone $$$
Lean4
@[deprecated ProperCone.isClosed (since := "2025-07-06")]
theorem isClosed_innerDualCone : IsClosed (s.innerDualCone : Set H) := by
-- reduce the problem to showing that dual cone of a singleton `{x}` is closed
rw [innerDualCone_eq_iInter_innerDualCone_singleton]
apply isClosed_iInter
intro x
have h : ({↑x} : Set H).innerDualCone = (inner ℝ (x : H)) ⁻¹' Set.Ici 0 := by
rw [innerDualCone_singleton, ConvexCone.coe_comap, ConvexCone.coe_positive, innerₛₗ_apply_coe]
-- the preimage is closed as `inner x` is continuous and `[0, ∞)` is closed
rw [h]
exact isClosed_Ici.preimage (continuous_const.inner continuous_id')
