antitoneOn_slope_lt — Mathlib

English

If f is concave on s, then the slope of the secant line through any x ∈ s is antitone on s \\ {x}.

Русский

Если f выпукла на s, то наклон секантной линии через x является антитонным на s \\ {x}.

LaTeX

$$$\\forall 𝕜,\\; \\text{ConcaveOn } 𝕜\\; s\\; f \\Rightarrow x\\in s \\Rightarrow \\text{AntitoneOn } (\\text{slope } f x)\\ (s \\setminus \\{x\\}).$$

Lean4

theorem antitoneOn_slope_lt (hfc : ConcaveOn 𝕜 s f) (hxs : x ∈ s) : AntitoneOn (slope f x) ({y ∈ s | y < x}) :=
  (hfc.slope_anti hxs).mono fun _ ⟨h1, h2⟩ ↦ ⟨h1, h2.ne⟩

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