lt_left_of_right_lt — Mathlib

English

If f is convex on s, and f(x) < f(z) with z on the segment between x and y, then f(z) < f(y).

Русский

Если f выпукла на s и f(x) < f(z) при z на отрезке между x и y, то f(z) < f(y).

LaTeX

$$$\ConvexOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y\in s, z\in openSegment(\mathfrak{K}, x, y): f(x) < f(z) \Rightarrow f(z) < f(y)$$$

Lean4

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

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