sub — 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 sub (hf : TorusIntegrable f c R) (hg : TorusIntegrable g c R) : TorusIntegrable (f - g) c R :=
  hf.sub hg

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