quasiconvexOn — Mathlib

English

If f is quasiconvex on S, then the sublevel set {x ∈ s : f(x) < r} is convex for every r.

Русский

Если f квазиконвексна на S, то подуровневое множество {x ∈ s : f(x) < r} выпукло для любого r.

LaTeX

$$$QuasiconvexOn\ 𝕜\ s\ f \rightarrow \forall r, Convex\ 𝕜\ {x\in s \mid f(x) < r}$$$

Lean4

theorem quasiconvexOn (hf : Monotone f) : QuasiconvexOn 𝕜 univ f :=
  (hf.monotoneOn _).quasiconvexOn convex_univ

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