contDiffAt_rpow_const — Mathlib

English

For every x ∈ ℝ and p ∈ ℝ, the function x ↦ x^p is ContDiffAt at x, provided x ≠ 0 or p is large enough to keep the expression well-defined.

Русский

Для каждого x ∈ ℝ и p ∈ ℝ функция x^p является ContDiffAt в x, если x ≠ 0 или p достаточно велик, чтобы выражение было определено.

LaTeX

$$$\\forall x\\in\\mathbb{R},\\forall p\\in\\mathbb{R},\\\\ x\\neq 0\\lor p\\ge 1\\Rightarrow ContDiffAt\\mathbb{R}\\,n\\ (x\\mapsto x^p)\\ x.$$$

Lean4

theorem contDiffAt_rpow_const {x p : ℝ} {n : ℕ} (h : x ≠ 0 ∨ ↑n ≤ p) : ContDiffAt ℝ n (fun x : ℝ => x ^ p) x :=
  h.elim contDiffAt_rpow_const_of_ne contDiffAt_rpow_const_of_le

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