convexOn_exp

Mathlib.Analysis.Convex.SpecificFunctions.Basic

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

English

Real exponentiation is convex on the real line.

Русский

Возведение экспоненты в действительное число выпукло на всей вещественной оси.

LaTeX

$$$\text{ConvexOn } \mathbb{R}\ \mathrm{univ}\ \exp$$$

Lean4

/-- `Real.exp` is convex on the whole real line. -/
theorem convexOn_exp : ConvexOn ℝ univ exp :=
  strictConvexOn_exp.convexOn

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

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

Разделы

Аффилиация

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