congr — Mathlib

English

If f is strictly convex, then its dual is strictly concave.

Русский

Если f строго выпукла, то ее двойственная функция строго конкавна.

LaTeX

$$$$ \\operatorname{StrictConvexOn}_{\\mathsf{𝕜}}(S,f) \\Rightarrow \\operatorname{StrictConcaveOn}_{\\mathsf{𝕜}}(S,\\mathrm{toDual}\\circ f). $$$$

Lean4

theorem congr (hf : ConcaveOn 𝕜 s f) (hfg : EqOn f g s) : ConcaveOn 𝕜 s g :=
  ⟨hf.1, fun x hx y hy a b ha hb hab => by
    simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab⟩

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