English
QuasiconvexOn 𝕜 s f is equivalent to convexity of s together with the condition that for all x,y ∈ s and a,b ≥ 0 with a+b=1, f(ax+by) ≤ max(f(x),f(y)).
Русский
QuasiconvexOn 𝕜 s f эквивалентна выпуклости s и условию: для всех x,y ∈ s и a,b ≥ 0 с a+b=1 верно f(ax+by) ≤ max(f(x),f(y)).
LaTeX
$$$QuasiconvexOn\ 𝕜\ s\ f \iff 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) \le \max(f(x),f(y))$$$
Lean4
theorem quasiconvexOn_iff_le_max :
QuasiconvexOn 𝕜 s f ↔
Convex 𝕜 s ∧
∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y) :=
⟨fun hf =>
⟨hf.convex, fun _ hx _ hy _ _ ha hb hab => (hf _ ⟨hx, le_max_left _ _⟩ ⟨hy, le_max_right _ _⟩ ha hb hab).2⟩,
fun hf _ _ hx _ hy _ _ ha hb hab =>
⟨hf.1 hx.1 hy.1 ha hb hab, (hf.2 hx.1 hy.1 ha hb hab).trans <| max_le hx.2 hy.2⟩⟩
