differentiableAt_rpow_of_ne — Mathlib

English

If p=(x,y) with x ≠ 0, then the map t ↦ t^p is differentiable at t = x in ℝ.

Русский

Пусть p=(x,y) с x ≠ 0; функция t ↦ t^p дифференцируема в t = x.

LaTeX

$$$\\text{Let } p=(x,y)\\text{ with } x\\neq 0.\\\\ \\text{Then } t\\mapsto t^{p}\\text{ is differentiable at } t=x.$$$

Lean4

theorem differentiableAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.1 ≠ 0) : DifferentiableAt ℝ (fun p : ℝ × ℝ => p.1 ^ p.2) p :=
  (contDiffAt_rpow_of_ne p hp).differentiableAt le_rfl

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