differentiableAt_const — Mathlib

English

For any n ∈ ℕ with OfNat F n, the constant map ofNat(n) is differentiable at x with derivative 0.

Русский

Для любого n ∈ ℕ c OfNat F n, константное отображение ofNat(n) дифференцируемо в точке x с нулевой производной.

LaTeX

$$DifferentiableAt 𝕜 (ofNat(n) : E → F) x$$

Lean4

@[simp, fun_prop]
theorem differentiableAt_const (c : F) : DifferentiableAt 𝕜 (fun _ => c) x :=
  ⟨0, hasFDerivAt_const c x⟩

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