hasFDerivAt_list_prod' — Mathlib

English

If a is differentiable, then the map y ↦ b · a(y) is differentiable everywhere (over 𝕜).

Русский

Если a дифференцируема, то отображение y ↦ b · a(y) дифференцируемо во всей области определения.

LaTeX

$$$\\text{Differentiable }\\mathbb{K}\\, a \\Rightarrow \\text{Differentiable }\\mathbb{K}\\, (\\lambda y. b \\cdot a(y))$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_list_prod' [Fintype ι] {l : List ι} {x : ι → 𝔸'} :
    HasFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)
      (∑ i : Fin l.length, ((l.take i).map x).prod • proj l[i] <• ((l.drop (.succ i)).map x).prod) x :=
  hasStrictFDerivAt_list_prod'.hasFDerivAt

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