lt_right_of_left_lt — Mathlib

English

Let f be concave on a set s. For any x, y in s and any z in the open segment between x and y, if f(z) < f(x), then f(y) < f(z).

Русский

Пусть f выпукла на s. Для любых x, y ∈ s и любого z ∈ openSegment(x,y), если f(z) < f(x), то f(y) < f(z).

LaTeX

$$$ConcaveOn\ 𝕜\ s\ f \Rightarrow \forall x\in s\,\forall y\in s\,\forall z\in openSegment\ 𝕜\ x\ y,\ f(z) < f(x) \rightarrow f(y) < f(z).$$$

Lean4

theorem lt_right_of_left_lt (hf : ConcaveOn 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y)
    (hxz : f z < f x) : f y < f z :=
  hf.dual.lt_right_of_left_lt hx hy hz hxz

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