strongConcaveOn_zero

Mathlib.Analysis.Convex.Strong

URI: https://scilib.ai/kg/mathlib#strongConcaveOn_zero

English

Strong convexity at zero modulus is equivalent to convexity.

Русский

Строгая выпуклость при нулевом модуле эквивалентна выпуклости.

LaTeX

$$$$ \text{StrongConvexOn}(s,0,f) \iff \text{ConvexOn}(\mathbb{R},s,f). $$$$

Lean4

@[simp]
theorem strongConcaveOn_zero : StrongConcaveOn s 0 f ↔ ConcaveOn ℝ s f := by simp [StrongConcaveOn, ← Pi.zero_def]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru