mathlib documentation

analysis.convex.body

convex bodies #

This file contains the definition of the type convex_body V consisting of convex, compact, nonempty subsets of a real normed space V.

convex_body V is a module over the nonnegative reals (nnreal).

TODOs:

Tags #

convex, convex body

structure convex_body (V : Type u_1) [seminormed_add_comm_group V] [normed_space V] :
Type u_1

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

Instances for convex_body
@[protected, ext]
theorem convex_body.ext {V : Type u_1} [seminormed_add_comm_group V] [normed_space V] {K L : convex_body V} (h : K = L) :
K = L
@[simp]
theorem convex_body.coe_mk {V : Type u_1} [seminormed_add_comm_group V] [normed_space V] (s : set V) (h₁ : convex s) (h₂ : is_compact s) (h₃ : s.nonempty) :
{carrier := s, convex' := h₁, is_compact' := h₂, nonempty' := h₃} = s
@[simp]
theorem convex_body.coe_add {V : Type u_1} [seminormed_add_comm_group V] [normed_space V] (K L : convex_body V) :
(K + L) = K + L
@[protected, instance]
Equations
@[simp]
theorem convex_body.coe_smul {V : Type u_1} [seminormed_add_comm_group V] [normed_space V] (c : ) (K : convex_body V) :
(c K) = c K
@[simp]
theorem convex_body.coe_smul' {V : Type u_1} [seminormed_add_comm_group V] [normed_space V] (c : nnreal) (K : convex_body V) :
(c K) = c K
@[protected, instance]

The convex bodies in a fixed space $V$ form a module over the nonnegative reals.

Equations