Theorems · Definition · convex and discrete geometry

ConvexOn

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

Convexity of functions

Defined in

Mathlib.Analysis.Convex.Function

Cited by

232 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 123 definitions · uses no axioms

Assumes

SemiringPartialOrderAddCommMonoidAddCommMonoidPartialOrderSMulSMul