neg

Mathlib.Analysis.BoxIntegral.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Integrable.neg

English

If hf is Integrable, then -f is Integrable and its integral is the negation of that of f.

Русский

Если hf интегрируемо, то −f интегрируемо, и его интеграл равен отрицанию интеграла от f.

LaTeX

$$$\mathrm{Integrable}(I,l,-f,vol) \iff \mathrm{Integrable}(I,l,f,vol)$$$

Lean4

theorem neg (hf : Integrable I l f vol) : Integrable I l (-f) vol :=
  hf.hasIntegral.neg.integrable

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru