quasiconvexOn_of_convex_le — Mathlib

English

If the codomain is directed and f is quasiconvex on s, then f is convex on s.

Русский

Если кодомен тщательно ориентирован и f квазиконвексна на s, то f выпукла на s.

LaTeX

$$$ [\IsDirected\ β (\cdot \le \cdot)] \Rightarrow \text{QuasiconvexOn } 𝕜 s f \Rightarrow \text{Convex } 𝕜 s $$$

Lean4

theorem quasiconvexOn_of_convex_le (hs : Convex 𝕜 s) (h : ∀ r, Convex 𝕜 {x | f x ≤ r}) : QuasiconvexOn 𝕜 s f := fun r =>
  hs.inter (h r)

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