Theorems · Definition · convex and discrete geometry

StrictConvex

(𝕜 : Type u_6) →
  {E : Type u_7} →
    [Semiring 𝕜] → [PartialOrder 𝕜] → [TopologicalSpace E] → [AddCommMonoid E] → [SMul 𝕜 E] → Set E → Prop

A set is strictly convex if the open segment between any two distinct points lies is in its interior. This basically means "convex and not flat on the boundary".

Defined in

Mathlib.Analysis.Convex.Strict

Cited by

71 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

SemiringPartialOrderTopologicalSpaceAddCommMonoidSMul