quasiconcaveOn_of_convex_ge — Mathlib

English

If s is convex and all superlevel sets {x in s | r ≤ f(x)} are convex for all r, then f is quasiconcave on s.

Русский

Если s выпукло и все суперуровни f(x) ≥ r выпуклы для всех r, то f является квазивогнутой на s.

LaTeX

$$$ Convex 𝕜 s \Rightarrow (\forall r, Convex 𝕜 {x \in s | r ≤ f(x)}) \Rightarrow QuasiconcaveOn 𝕜 s f $$$

Lean4

theorem quasiconcaveOn_of_convex_ge (hs : Convex 𝕜 s) (h : ∀ r, Convex 𝕜 {x | r ≤ f x}) : QuasiconcaveOn 𝕜 s f :=
  Convex.quasiconvexOn_of_convex_le (β := βᵒᵈ) hs h

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