# Closure of cones #

We define the closures of convex and pointed cones. This construction is primarily needed for defining maps between proper cones. The current API is basic and should be extended as necessary.

def
ConvexCone.closure
{𝕜 : Type u_1}
[OrderedSemiring 𝕜]
{E : Type u_2}
[AddCommMonoid E]
[TopologicalSpace E]
[ContinuousAdd E]
[SMul 𝕜 E]
[ContinuousConstSMul 𝕜 E]
(K : ConvexCone 𝕜 E)
:

ConvexCone 𝕜 E

The closure of a convex cone inside a topological space as a convex cone. This construction is mainly used for defining maps between proper cones.

## Instances For

@[simp]

theorem
ConvexCone.coe_closure
{𝕜 : Type u_1}
[OrderedSemiring 𝕜]
{E : Type u_2}
[AddCommMonoid E]
[TopologicalSpace E]
[ContinuousAdd E]
[SMul 𝕜 E]
[ContinuousConstSMul 𝕜 E]
(K : ConvexCone 𝕜 E)
:

@[simp]

theorem
ConvexCone.mem_closure
{𝕜 : Type u_1}
[OrderedSemiring 𝕜]
{E : Type u_2}
[AddCommMonoid E]
[TopologicalSpace E]
[ContinuousAdd E]
[SMul 𝕜 E]
[ContinuousConstSMul 𝕜 E]
{K : ConvexCone 𝕜 E}
{a : E}
:

@[simp]

theorem
ConvexCone.closure_eq
{𝕜 : Type u_1}
[OrderedSemiring 𝕜]
{E : Type u_2}
[AddCommMonoid E]
[TopologicalSpace E]
[ContinuousAdd E]
[SMul 𝕜 E]
[ContinuousConstSMul 𝕜 E]
{K : ConvexCone 𝕜 E}
{L : ConvexCone 𝕜 E}
:

theorem
PointedCone.toConvexCone_closure_pointed
{𝕜 : Type u_1}
[OrderedSemiring 𝕜]
{E : Type u_2}
[AddCommMonoid E]
[TopologicalSpace E]
[ContinuousAdd E]
[Module 𝕜 E]
[ContinuousConstSMul 𝕜 E]
(K : PointedCone 𝕜 E)
:

(↑K).closure.Pointed

def
PointedCone.closure
{𝕜 : Type u_1}
[OrderedSemiring 𝕜]
{E : Type u_2}
[AddCommMonoid E]
[TopologicalSpace E]
[ContinuousAdd E]
[Module 𝕜 E]
[ContinuousConstSMul 𝕜 E]
(K : PointedCone 𝕜 E)
:

PointedCone 𝕜 E

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.

## Equations

- K.closure = ConvexCone.toPointedCone ⋯

## Instances For

@[simp]

theorem
PointedCone.coe_closure
{𝕜 : Type u_1}
[OrderedSemiring 𝕜]
{E : Type u_2}
[AddCommMonoid E]
[TopologicalSpace E]
[ContinuousAdd E]
[Module 𝕜 E]
[ContinuousConstSMul 𝕜 E]
(K : PointedCone 𝕜 E)
:

@[simp]

theorem
PointedCone.mem_closure
{𝕜 : Type u_1}
[OrderedSemiring 𝕜]
{E : Type u_2}
[AddCommMonoid E]
[TopologicalSpace E]
[ContinuousAdd E]
[Module 𝕜 E]
[ContinuousConstSMul 𝕜 E]
{K : PointedCone 𝕜 E}
{a : E}
:

@[simp]

theorem
PointedCone.closure_eq
{𝕜 : Type u_1}
[OrderedSemiring 𝕜]
{E : Type u_2}
[AddCommMonoid E]
[TopologicalSpace E]
[ContinuousAdd E]
[Module 𝕜 E]
[ContinuousConstSMul 𝕜 E]
{K : PointedCone 𝕜 E}
{L : PointedCone 𝕜 E}
: