Theorems · Theorem · convex and discrete geometry

StarConvex.smul

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E}, StarConvex 𝕜 x s → ∀ (c : 𝕜), StarConvex 𝕜 (c • x) (c • s)

Defined in

Mathlib.Analysis.Convex.Star

Cited by

2 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringPartialOrderAddCommMonoidModule