∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [inst_6 : SMul 𝕜 E]
  [inst_7 : SMul 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄,
            y ∈ s →
              ∀ ⦃a b : 𝕜⦄,
                0 ≤ a →
                  0 ≤ b →
                    0 < a + b → (a / (a + b)) • f x + (b / (a + b)) • f y ≤ f ((a / (a + b)) • x + (b / (a + b)) • y)