le_right_of_left_le'' — Mathlib

English

If f is convex on a convex set, then for x≤y≤z in the domain with x<y<z and f(x)≤f(y) we get f(y)≤f(z).

Русский

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

LaTeX

$$$$\\text{If } f\\text{ is convex on } s, \\; x,y,z\\in s,\\; x\\le y\\le z,\\; x

Lean4

theorem le_right_of_left_le'' (hf : ConvexOn 𝕜 s f) (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y ≤ z)
    (h : f x ≤ f y) : f y ≤ f z :=
  hyz.eq_or_lt.elim (fun hyz => (congr_arg f hyz).le) fun hyz =>
    hf.le_right_of_left_le hx hz (Ioo_subset_openSegment ⟨hxy, hyz⟩) h

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