monotoneOn_slope_gt — Mathlib

English

If f is convex on s and x ∈ s, then the slope at x is monotone on {y ∈ s | x < y}.

Русский

Если f выпукла на s и x ∈ s, тогда наклон в x монотонен на множ. {y ∈ s | x < y}.

LaTeX

$$$\\forall 𝕜,\\; \\text{ConvexOn } 𝕜\\; s\\; f \\Rightarrow x\\in s \\Rightarrow \\text{MonotoneOn } (\\text{slope } f x)\\ ({y ∈ s | x < y}).$$

Lean4

theorem monotoneOn_slope_gt (hfc : ConvexOn 𝕜 s f) (hxs : x ∈ s) : MonotoneOn (slope f x) ({y ∈ s | x < y}) :=
  (hfc.slope_mono hxs).mono fun _ ⟨h1, h2⟩ ↦ ⟨h1, h2.ne'⟩

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