rpow_const_of_le — Mathlib

English

If hf is ContDiff and h: m ≤ p, then the function x ↦ f x^p is ContDiff.

Русский

Если hf ∈ ContDiff и h: m ≤ p, то f^p дифференцируема.

LaTeX

$$ContDiff Real m.cast f x → Real.instLE.le m.cast p → ContDiff Real m.cast fun x => instHPow.hPow (f x) p$$

Lean4

@[fun_prop]
theorem rpow_const_of_le (hf : ContDiff ℝ m f) (h : ↑m ≤ p) : ContDiff ℝ m fun x => f x ^ p :=
  contDiff_iff_contDiffAt.mpr fun _ => hf.contDiffAt.rpow_const_of_le h

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