English
QuasilinearOn 𝕜 s f holds if and only if f is convex on s and f(a x + b y) ∈ uIcc(f(x), f(y)) for all x,y ∈ s and a,b ≥ 0 with a+b=1.
Русский
QuasilinearOn 𝕜 s f эквивалентно тому, что f выпукла на s и для любых x,y ∈ s и a,b ≥ 0 с a+b=1 имеет f(a x + b y) ∈ uIcc(f(x), f(y)).
LaTeX
$$$QuasilinearOn\ 𝕜\ s\ f \iff \Big( Convex\ 𝕜\ s \land \forall\{x\}, x\in s \to \forall\{y\}, y\in s \to \forall\{a,b\}: 𝕜, 0\le a \to 0\le b \to a+b=1 \to f(a\cdot x+b\cdot y) \in uIcc(f(x),f(y)) \Big)$$$
Lean4
theorem quasilinearOn_iff_mem_uIcc :
QuasilinearOn 𝕜 s f ↔
Convex 𝕜 s ∧
∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y) :=
by
rw [QuasilinearOn, quasiconvexOn_iff_le_max, quasiconcaveOn_iff_min_le, and_and_and_comm, and_self_iff]
apply and_congr_right'
simp_rw [← forall_and, ← Icc_min_max, mem_Icc, and_comm]
