Theorems · Definition · convex and discrete geometry

StarConvex

(𝕜 : Type u_4) → {E : Type u_5} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [SMul 𝕜 E] → E → Set E → Prop

Star-convexity of sets. s is star-convex at x if every segment from x to a point in s is contained in s.

Defined in

Mathlib.Analysis.Convex.Star

Cited by

62 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

SemiringPartialOrderAddCommMonoidSMul