pointed_toConvexCone — Mathlib

English

Every proper cone C, when regarded as a convex cone in the same space, is pointed (no nonzero vector lies in both C and its negative).

Русский

Каждый правильный конус C, рассматриваемый как выпуклый конус в той же пространстве, остроконечен (нет ненулевого вектора, который принадлежал бы как C, так и −C).

LaTeX

$$$(C : Set\,E) \cap (-(C : Set\,E)) = \{0\}$$$

Lean4

theorem pointed_toConvexCone (C : ProperCone R E) : (C : ConvexCone R E).Pointed :=
  C.toPointedCone.pointed_toConvexCone

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