Theorems · Inductive type · convex and discrete geometry

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.

Defined in

Mathlib.Analysis.Convex.Body

Cited by

29 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceAddCommMonoidSMul