dual — Mathlib

English

If a function f is convex on a set S, then its dual (with respect to the order) is concave on S; i.e., the composition with the order dual transforms convexity into concavity.

Русский

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

LaTeX

$$$$ \\operatorname{ConvexOn}_{\\mathsf{𝕜}}(S,f) \\;\;\\Rightarrow\\; \\operatorname{ConcaveOn}_{\\mathsf{𝕜}}(S,\\mathrm{toDual}\\circ f). $$$$

Lean4

theorem dual (hf : ConvexOn 𝕜 s f) : ConcaveOn 𝕜 s (toDual ∘ f) :=
  hf

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