add — Mathlib

English

If f and g are torus integrable then f + g is torus integrable.

Русский

Если f и g торусно интегрируемы, то f + g торусно интегрируемо.

LaTeX

$$$\operatorname{TorusIntegrable}(f,c,R) \land \operatorname{TorusIntegrable}(g,c,R) \Rightarrow \operatorname{TorusIntegrable}(f+g,c,R)$$$

Lean4

/-- If `f` and `g` are two torus integrable functions, then so is `f + g`. -/
protected nonrec theorem add (hf : TorusIntegrable f c R) (hg : TorusIntegrable g c R) : TorusIntegrable (f + g) c R :=
  hf.add hg

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