add — Mathlib

English

If f and g are differentiable-continuous-on-closure on a set, then their sum is differentiable-cont-on-closure on the same set.

Русский

Если функции f и g дифференцируемы-но на замыкании множества, то их сумма дифференцируема-но на замыкании того же множества.

LaTeX

$$$$\\text{If } DiffContOnCl\\ 𝕜\\ f\\ s\\ and\\ DiffContOnCl\\ 𝕜\\ g\\ s,\\ then } DiffContOnCl\\ 𝕜\\ (f+g)\\ s. $$$$

Lean4

theorem add (hf : DiffContOnCl 𝕜 f s) (hg : DiffContOnCl 𝕜 g s) : DiffContOnCl 𝕜 (f + g) s :=
  ⟨hf.1.add hg.1, hf.2.add hg.2⟩

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