convex_ge — Mathlib

English

Right translating the domain preserves concavity: a concave function remains concave after translating the domain to the right.

Русский

Правое перемещение домена сохраняет конкавность: конкавная функция остаётся конкавной после переноса вправо.

LaTeX

$$$hf.dual.translate_right\ _$$$

Lean4

theorem convex_ge (hf : ConcaveOn 𝕜 s f) (r : β) : Convex 𝕜 ({x ∈ s | r ≤ f x}) :=
  hf.dual.convex_le r

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