QuasilinearOn — Mathlib

English

A function is quasilinear on a set if it is both quasiconvex and quasiconcave; taking dual preserves this property.

Русский

Функция на множестве квазиконвексна и квазивогнута одновременно; переход к двойственному порядку сохраняет это свойство.

LaTeX

$$$ \text{QuasilinearOn} \ 𝕜 \ s \ f \Rightarrow \text{QuasilinearOn} \ 𝕜 \ s \ (toDual \circ f) $$$

Lean4

/-- A function is quasilinear if it is both quasiconvex and quasiconcave.
This means that, for all `r`,
the sets `{x ∈ s | f x ≤ r}` and `{x ∈ s | r ≤ f x}` are `𝕜`-convex. -/
def QuasilinearOn : Prop :=
  QuasiconvexOn 𝕜 s f ∧ QuasiconcaveOn 𝕜 s f

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