convexOn — Mathlib

English

If a function is uniformly convex on a set with a nonnegative modulus, then it is convex on that set.

Русский

Если функция униформно выпукла на некотором множестве с неположенным модулем, то она выпукла на этом множестве.

LaTeX

$$$$ \text{UniformConvexOn}(s,\phi,f) \land 0 \le \phi \Rightarrow \text{ConvexOn}(\mathbb{R},s,f). $$$$

Lean4

theorem convexOn (hf : UniformConvexOn s φ f) (hφ : 0 ≤ φ) : ConvexOn ℝ s f := by simpa using hf.mono hφ

Похожие утверждения