convex — Mathlib

English

Let S be a subset of a vector space E and f a function from E to a directed ordered semiring β. If f is quasiconcave on S, then S is convex (in the sense of 𝕜-convexity).

Русский

Пусть S ⊆ E и f: E → β. Если f квазиконкавна на S, то множество S выпукло (с точки зрения выпуквости относительно 𝕜).

LaTeX

$$$QuasiconcaveOn\ 𝕜\ s\ f \rightarrow Convex\ 𝕜\ s$$$

Lean4

theorem convex [IsDirected β (· ≥ ·)] (hf : QuasiconcaveOn 𝕜 s f) : Convex 𝕜 s :=
  hf.dual.convex

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