dual — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem dual (hf : StrictConcaveOn 𝕜 s f) : StrictConvexOn 𝕜 s (toDual ∘ f) :=
  hf

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