∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V]
  [inst_3 : ContinuousSMul ℝ V] [inst_4 : ContinuousAdd V] (c d : NNReal) (K : ConvexBody V),
  (c + d) • K = c • K + d • K