strictMonoOn_of_deriv_pos — Mathlib

English

Let D be a convex subset of R. If a function f is continuous on D, differentiable on the interior of D, and its derivative is strictly positive on the interior of D, then f is strictly increasing on D; that is, for any x < y in D, f(x) < f(y).

Русский

Пусть D — конвексное подмножество R. Если функция f непрерывна на D, дифференцируема в interior(D) и производная f’ положительна на interior(D), тогда f строго возрастает на D; то есть для любых x < y из D выполняется f(x) < f(y).

LaTeX

$$$\text{Let } D \subseteq \mathbb{R} \,\text{ convex},\; f: \mathbb{R} \to \mathbb{R}, \; f \text{ continuous on } D, \; f \text{ differentiable on } \operatorname{int} D, \; 0 < f'(x) \text{ for all } x \in \operatorname{int} D.\\ \text{Then } f \text{ is strictly monotone on } D, i.e. } x

Lean4

/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is positive, then
`f` is a strictly monotone function on `D`.
Note that we don't require differentiability explicitly as it already implied by the derivative
being strictly positive. -/
theorem strictMonoOn_of_deriv_pos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
    (hf' : ∀ x ∈ interior D, 0 < deriv f x) : StrictMonoOn f D :=
  by
  intro x hx y hy
  have : DifferentiableOn ℝ f (interior D) := fun z hz =>
    (differentiableAt_of_deriv_ne_zero (hf' z hz).ne').differentiableWithinAt
  simpa only [zero_mul, sub_pos] using hD.mul_sub_lt_image_sub_of_lt_deriv hf this hf' x hx y hy

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