innerDualCone_of_innerDualCone_eq_self

English

If K is a nonempty closed convex cone, then taking the inner dual twice returns K: (K.innerDualCone).innerDualCone = K.

Русский

Если K — непустой замкнутый выпуклый конус, то применение двойственного конуса дважды возвращает исходный K.

LaTeX

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

Lean4

/-- The inner dual of inner dual of a non-empty, closed convex cone is itself. -/
@[deprecated ProperCone.innerDual_innerDual (since := "2025-07-06")]
theorem innerDualCone_of_innerDualCone_eq_self (K : ConvexCone ℝ H) (ne : (K : Set H).Nonempty)
    (hc : IsClosed (K : Set H)) : ((K : Set H).innerDualCone : Set H).innerDualCone = K :=
  by
  ext x
  constructor
  · rw [mem_innerDualCone, ← SetLike.mem_coe]
    contrapose!
    exact K.hyperplane_separation_of_nonempty_of_isClosed_of_notMem ne hc
  · rintro hxK y h
    specialize h x hxK
    rwa [real_inner_comm]

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