toConvexCone_closure_pointed — Mathlib

English

The closure of a pointed cone, when viewed as a convex cone, is again a pointed cone.

Русский

Замыкание указательного конуса, рассматриваемое как выпуклый конус, вновь является указательным конусом.

LaTeX

$$(K : ConvexCone 𝕜 E).closure.Pointed$$

Lean4

theorem toConvexCone_closure_pointed (K : PointedCone 𝕜 E) : (K : ConvexCone 𝕜 E).closure.Pointed :=
  subset_closure <| PointedCone.pointed_toConvexCone _

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