differentiableOn_zpow — Mathlib

English

The function x ↦ x^m is differentiable on a set s provided either 0 ∉ s or m ≥ 0.

Русский

Функция x ↦ x^m дифференцируема на множество s при условии либо 0 не принадлежит s, либо m ≥ 0.

LaTeX

$$$(0 : 𝕜) \\notin s \\lor 0 \\le m \\Rightarrow \\text{DifferentiableOn } 𝕜 (\\lambda x, x^m) s$$$

Lean4

theorem differentiableOn_zpow (m : ℤ) (s : Set 𝕜) (h : (0 : 𝕜) ∉ s ∨ 0 ≤ m) : DifferentiableOn 𝕜 (fun x => x ^ m) s :=
  fun x hxs => differentiableWithinAt_zpow m x <| h.imp_left <| ne_of_mem_of_not_mem hxs

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