Theorems · Theorem · convex and discrete geometry

Convex_subadditive_le

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : LinearOrder 𝕜]
  [IsOrderedRing 𝕜] [inst_4 : SMul 𝕜 E] {f : E → 𝕜},
  (∀ (x y : E), f (x + y) ≤ f x + f y) →
    (∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x) → ∀ (B : 𝕜), Convex 𝕜 {x | f x ≤ B}

Defined in

Mathlib.Analysis.Convex.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidLinearOrderIsOrderedRingSMul