norm_image_sub_le_of_norm_deriv_le_segment_01

English

If a differentiable function on [a,b] has zero derivative inside every interior point of [a,b], then f is constant on [a,b], i.e. f(x)=f(a).

Русский

Если производная внутри равна нулю в каждой точке интервала, функция постоянна на [a,b], то f(x)=f(a).

LaTeX

$$$\displaystyle \forall x\in[a,b],\; f(x)=f(a)$, given HasDerivWithinAt f 0 on the interior.$$

Lean4

/-- A function on `[0, 1]` with the norm of the derivative within `[0, 1]`
bounded by `C` satisfies `‖f 1 - f 0‖ ≤ C`, `derivWithin` version. -/
theorem norm_image_sub_le_of_norm_deriv_le_segment_01 {C : ℝ} (hf : DifferentiableOn ℝ f (Icc (0 : ℝ) 1))
    (bound : ∀ x ∈ Ico (0 : ℝ) 1, ‖derivWithin f (Icc (0 : ℝ) 1) x‖ ≤ C) : ‖f 1 - f 0‖ ≤ C := by
  simpa only [sub_zero, mul_one] using
    norm_image_sub_le_of_norm_deriv_le_segment hf bound 1 (right_mem_Icc.2 zero_le_one)

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