of_neg

Mathlib.Analysis.BoxIntegral.Basic

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

English

If HasIntegral I l f vol y holds, then HasIntegral I l (-f) vol (-y) holds.

Русский

Если HasIntegral для f существует, то существует HasIntegral для −f и −y.

LaTeX

$$$\mathrm{HasIntegral}(I,l,f,vol,y) \Rightarrow \mathrm{HasIntegral}(I,l,-f,vol,-y)$$$

Lean4

theorem of_neg (hf : Integrable I l (-f) vol) : Integrable I l f vol :=
  neg_neg f ▸ hf.neg

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

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

Разделы

Аффилиация

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