Theorems · Definition · convex and discrete geometry

ConvexCone.closure

{𝕜 : Type u_1} →
  [inst : Semiring 𝕜] →
    [inst_1 : PartialOrder 𝕜] →
      {E : Type u_2} →
        [inst_2 : AddCommMonoid E] →
          [inst_3 : TopologicalSpace E] →
            [ContinuousAdd E] → [inst_5 : SMul 𝕜 E] → [ContinuousConstSMul 𝕜 E] → 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.

Defined in

Mathlib.Analysis.Convex.Cone.Closure

Cited by

4 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringPartialOrderAddCommMonoidTopologicalSpaceContinuousAddSMulContinuousConstSMul