dual_flip_dual — Mathlib

English

The double dual of a proper cone is the cone itself: dual p (dual p.flip (C)) = C.

Русский

Двойной дуал нормального конуса равен самому конусу: dual p (dual p.flip (C)) = C.

LaTeX

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

Lean4

/-- The **double dual of a proper cone** is itself. -/
@[simp]
theorem dual_flip_dual (p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [p.IsContPerfPair] (C : ProperCone ℝ E) :
    dual p.flip (dual p (C : Set E)) = C :=
  by
  refine le_antisymm (fun x ↦ ?_) subset_dual_dual
  simp only [mem_toPointedCone, mem_dual, SetLike.mem_coe]
  contrapose!
  simpa [p.flip.toContPerfPair.surjective.exists] using C.hyperplane_separation_point

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