contDiffAt_rpow_const_of_le — Mathlib

English

For p ∈ ℝ and n ∈ ℕ, if n ≤ p then ContDiffAt ℝ n (x ↦ x^p) at any x.

Русский

Для p ∈ ℝ и n ∈ ℕ, если n ≤ p, то ContDiffAt ℝ n (x^p) в любой точке.

LaTeX

$$$\\forall p\\in\\mathbb{R},\\forall n\\in\\mathbb{N},\\ n\\le p\\Rightarrow ContDiffAt\\mathbb{R}\\,n\\ (x\\mapsto x^p)\\ x$.$$

Lean4

theorem contDiffAt_rpow_const_of_le {x p : ℝ} {n : ℕ} (h : ↑n ≤ p) : ContDiffAt ℝ n (fun x : ℝ => x ^ p) x :=
  (contDiff_rpow_const_of_le h).contDiffAt

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