le_left_of_right_le'' — Mathlib

English

If a function is convex on a set, then along a chain x≤y≤z with x<y≤z and f(x)≤f(y) one gets f(y)≤f(z).

Русский

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

LaTeX

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

Lean4

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

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