Theorems · Definition · convex and discrete geometry

QuasilinearOn

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

A function is quasilinear if it is both quasiconvex and quasiconcave. This means that, for all r, the sets {x ∈ s | f x ≤ r} and {x ∈ s | r ≤ f x} are 𝕜-convex.

Defined in

Mathlib.Analysis.Convex.Quasiconvex

Cited by

11 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

SemiringPartialOrderAddCommMonoidLESMul