closure — Mathlib

English

The closure operation on PointedCones yields a new PointedCone; i.e., closure(K) is a PointedCone.

Русский

Операция замыкания над PointedCone даёт новый PointedCone; то есть closure(K) является указательным конусом.

LaTeX

$$PointedCone.closure(K) is a PointedCone 𝕜 E$$

Lean4

/-- The closure of a pointed cone inside a topological space as a pointed cone. This
construction is mainly used for defining maps between proper cones. -/
protected def closure (K : PointedCone 𝕜 E) : PointedCone 𝕜 E :=
  K.toConvexCone.closure.toPointedCone K.toConvexCone_closure_pointed

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