quasilinearOn — Mathlib

English

QuasilinearOn 𝕜 s f is equivalent to convexity of s and the image under f of convex combinations lies in the closed interval between f(x) and f(y).

Русский

QuasilinearOn 𝕜 s f эквивалентно выпуклости S и тому, что f(a x + b y) belongs to uIcc(f(x), f(y)).

LaTeX

$$$QuasilinearOn\ 𝕜\ s\ f \iff Convex\ 𝕜\ s \land ∀ {x} , x\in s \rightarrow ∀ {y}, y\in s \rightarrow ∀ {a b : 𝕜}, 0 \le a \to 0 \le b \to a+b = 1 \to f(a\cdot x + b\cdot y) ∈ uIcc (f x) (f y)$$$

Lean4

theorem quasilinearOn (hf : AntitoneOn f s) (hs : Convex 𝕜 s) : QuasilinearOn 𝕜 s f :=
  ⟨hf.quasiconvexOn hs, hf.quasiconcaveOn hs⟩

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