English
If for all i in a finite set s the functions f_i are ContDiffWithinAt 𝕜 n at x on s, then the sum over i in s of f_i is ContDiffWithinAt 𝕜 n at x on s.
Русский
Если для всех i в конечном множестве s функции f_i являются ContDiffWithinAt 𝕜 n на области s в точке x, то сумма ∑_{i∈s} f_i также ContDiffWithinAt 𝕜 n на области s в точке x.
LaTeX
$$$\forall i ∈ s, ContDiffWithinAt 𝕜 n (f_i) s x \Rightarrow ContDiffWithinAt 𝕜 n (\sum_{i∈s} f_i) s x$$$
Lean4
/-- The difference of two `C^n` functions within a set at a point is `C^n` within this set
at this point. -/
@[fun_prop]
theorem sub {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 := by simpa only [sub_eq_add_neg] using hf.add hg.neg
