uniformConvexOn_zero — Mathlib

English

UniformConvexOn s 0 f is equivalent to ConvexOn Real s f; i.e., uniform convexity with zero modulus reduces to ordinary convexity.

Русский

Унитарная выпуклость с нулевым модулем эквивалентна обычной выпуклости на s.

LaTeX

$$$UniformConvexOn s 0 f \iff ConvexOn Real s f$$$

Lean4

@[simp]
theorem uniformConvexOn_zero : UniformConvexOn s 0 f ↔ ConvexOn ℝ s f := by simp [UniformConvexOn, ConvexOn]

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