add — Mathlib

English

The map f ↦ f(i) j is ContDiff 𝕜 n.

Русский

Отображение f ↦ f(i) j является ContDiff 𝕜 n.

LaTeX

$$$\text{ContDiff } 𝕜 n (\lambda f, f(i)(j))$$$

Lean4

/-- The sum of two `C^n` functions within a set at a point is `C^n` within this set
at this point. -/
@[fun_prop]
theorem add {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
    ContDiffWithinAt 𝕜 n (fun x => f x + g x) s x :=
  contDiff_add.contDiffWithinAt.comp x (hf.prodMk hg) subset_preimage_univ

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