Documentation

Mathlib.Analysis.Convex.Cone.Closure

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.

Equations
  • K.closure = { carrier := closure K, smul_mem' := , add_mem' := }
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) :
    K.closure = closure K
    @[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} :
    a K.closure a closure K
    @[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} :
    K.closure = L closure K = L
    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) :

    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
    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) :
      K.closure = closure K
      @[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} :
      a K.closure a closure K
      @[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} :
      K.closure = L closure K = L