convex — Mathlib

English

If β is directed, then a quasiconvex function on s implies convexity on s.

Русский

Если β направлен, то квазиконвексная функция на s подразумевает выпуклость на s.

LaTeX

$$$ [\IsDirected β (≤)] \Rightarrow (hf : QuasiconvexOn 𝕜 s f) \Rightarrow Convex 𝕜 s $$$

Lean4

theorem convex [IsDirected β (· ≤ ·)] (hf : QuasiconvexOn 𝕜 s f) : Convex 𝕜 s := fun x hx y hy _ _ ha hb hab =>
  let ⟨_, hxz, hyz⟩ := exists_ge_ge (f x) (f y)
  (hf _ ⟨hx, hxz⟩ ⟨hy, hyz⟩ ha hb hab).1

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