dual_dual_flip — Mathlib

English

The double dual of a proper cone yields the original cone, mirroring the previous dual-flip result.

Русский

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

LaTeX

$$dual p (dual p.flip (C)) = C$$

Lean4

/-- The **double dual of a proper cone** is itself. -/
@[simp]
theorem dual_dual_flip (p : F →ₗ[ℝ] E →ₗ[ℝ] ℝ) [p.IsContPerfPair] (C : ProperCone ℝ E) :
    dual p (dual p.flip (C : Set E)) = C :=
  C.dual_flip_dual p.flip

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