translate_right — Mathlib

English

Right translation preserves strict concavity.

Русский

Правое перемещение сохраняет строгую конкавность.

LaTeX

$$$StrictConcaveOn\ 𝕜\ s\ f \Rightarrow \forall c\, StrictConcaveOn\ 𝕜\ (Set.preimage(\lambda z. c + z)\ s)\ (f \circ (\lambda z. c + z))$$$

Lean4

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

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