innerDual_innerDual — Mathlib

English

The inner dual cone of the inner dual cone of a proper cone C returns to C.

Русский

Двойной конус двойного конуса правильного конуса C возвращает C.

LaTeX

$$$\\text{innerDual}(\\text{innerDual}(C))=C$$$

Lean4

/-- The inner dual of inner dual of a proper cone is itself. -/
@[simp]
theorem innerDual_innerDual (C : ProperCone ℝ E) : innerDual (innerDual (C : Set E)) = C := by
  simpa using C.dual_flip_dual (innerₗ E)

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