Documentation

Mathlib.Analysis.Convex.Body

Convex bodies #

This file contains the definition of the type ConvexBody V consisting of convex, compact, nonempty subsets of a real topological vector space V.

ConvexBody V is a module over the nonnegative reals (NNReal) and a pseudo-metric space. If V is a normed space, ConvexBody V is a metric space.

TODO #

Tags #

convex, convex body

structure ConvexBody (V : Type u_2) [TopologicalSpace V] [AddCommMonoid V] [SMul V] :
Type u_2

Let V be a real topological vector space. A subset of V is a convex body if and only if it is convex, compact, and nonempty.

Instances For
    theorem ConvexBody.ext {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] {K : ConvexBody V} {L : ConvexBody V} (h : K = L) :
    K = L
    @[simp]
    theorem ConvexBody.coe_mk {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] (s : Set V) (h₁ : Convex s) (h₂ : IsCompact s) (h₃ : Set.Nonempty s) :
    { carrier := s, convex' := h₁, isCompact' := h₂, nonempty' := h₃ } = s
    theorem ConvexBody.coe_nsmul {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousAdd V] (n : ) (K : ConvexBody V) :
    ↑(n K) = n K
    @[simp]
    theorem ConvexBody.coe_add {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousAdd V] (K : ConvexBody V) (L : ConvexBody V) :
    ↑(K + L) = K + L
    @[simp]
    theorem ConvexBody.coe_zero {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] :
    0 = 0
    @[simp]
    theorem ConvexBody.coe_smul {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousSMul V] (c : ) (K : ConvexBody V) :
    ↑(c K) = c K
    @[simp]
    theorem ConvexBody.coe_smul' {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousSMul V] [ContinuousAdd V] (c : NNReal) (K : ConvexBody V) :
    ↑(c K) = c K