strongConvexOn_zero

Mathlib.Analysis.Convex.Strong

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

English

Strong convexity with zero modulus is equivalent to ordinary convexity.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem strongConvexOn_zero : StrongConvexOn s 0 f ↔ ConvexOn ℝ s f := by simp [StrongConvexOn, ← Pi.zero_def]

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

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

Разделы

Аффилиация

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