neg — Mathlib

English

If f is torus integrable with center c and radius R, then -f is torus integrable with the same center and radius.

Русский

Если f есть торусно интегрируемая функция с центром c и радиусом R, то -f тоже торусно интегрируема при тех же параметрах.

LaTeX

$$$\operatorname{TorusIntegrable}(f,c,R) \Rightarrow \operatorname{TorusIntegrable}(-f,c,R)$$$

Lean4

/-- If `f` is torus integrable then `-f` is torus integrable. -/
protected nonrec theorem neg (hf : TorusIntegrable f c R) : TorusIntegrable (-f) c R :=
  hf.neg

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