ProperCone — Mathlib

English

There is a canonical equivalence between a proper cone and its associated pointed cone, given by the natural coercion.

Русский

Существует природное соответствие между правильным конусом и связанным с ним точечным конусом, задаваемое естественной вложением.

LaTeX

$$$\text{toPointedCone} : ProperCone(R,E) \to PointedCone(R,E)$$$

Lean4

/-- A proper cone is a pointed cone `C` that is closed. Proper cones have the nice property that
they are equal to their double dual, see `ProperCone.dual_dual`.
This makes them useful for defining cone programs and proving duality theorems. -/
abbrev ProperCone :=
  ClosedSubmodule R≥0 E

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