lt_right_of_left_lt — Mathlib

English

A convex function on a segment yields an inequality of the type f(y) > f(z) whenever z lies between x and y and f(x) < f(z).

Русский

Выпуклая функция на отрезке дает неравенство вида f(y) > f(z) когда z лежит между x и y и f(x) < f(z).

LaTeX

$$$\ConvexOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y,z:\ openSegment(\mathfrak{K}, x, y) \text{ условия} \Rightarrow f(z) < f(y)$$$

Lean4

theorem lt_right_of_left_lt (hf : ConvexOn 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y)
    (hxz : f x < f z) : f z < f y := by
  obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
  exact hf.lt_right_of_left_lt' hx hy ha hb hab hxz

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