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.

source
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
    source
    @[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
    source
    @[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
    source
    @[simp]
    theorem ConvexCone.closure_eq {𝕜 : Type u_1} [OrderedSemiring 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] [SMul 𝕜 E] [ContinuousConstSMul 𝕜 E] {K L : ConvexCone 𝕜 E} :
    K.closure = L ↔ closure ↑K = ↑L
    source
    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
    source
    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
    Instances For
      source
      @[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
      source
      @[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
      source
      @[simp]
      theorem PointedCone.closure_eq {𝕜 : Type u_1} [OrderedSemiring 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] [Module 𝕜 E] [ContinuousConstSMul 𝕜 E] {K L : PointedCone 𝕜 E} :
      K.closure = L ↔ closure ↑K = ↑L