coe_dual — Mathlib

English

For a proper cone K, the inner dual structure yields the equality innerDual(innerDual(K)) = K.

Русский

Для конуса K справедливо: внутреннее двойственное конусное преобразование дважды возвращает исходный конус.

LaTeX

$$$ innerDual(innerDual(K)) = K $$$

Lean4

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

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