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