translate_right

Mathlib.Analysis.Convex.Function

URI: https://scilib.ai/kg/mathlib#ConcaveOn.translate_right

← MathLib Explorer

English

If f is concave on s, then f plus a constant is concave on s.

Русский

Если f конкавна на s, то f + константа конкавна на s.

LaTeX

$$$ConcaveOn\ 𝕜\ s\ f \rightarrow ConcaveOn\ 𝕜\ s\ (f + fun _ => b)$$$

Lean4

/-- Right translation preserves concavity. -/
theorem translate_right (hf : ConcaveOn 𝕜 s f) (c : E) : ConcaveOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => c + z) :=
  hf.dual.translate_right _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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