hasIntegral_zero

Mathlib.Analysis.BoxIntegral.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.hasIntegral_zero

English

HasIntegral for the zero function exists: HasIntegral I l (fun _ => 0) vol 0.

Русский

Существует интеграл для нулевой функции: HasIntegral I l (функция, возвращающая 0) vol 0.

LaTeX

$$$\text{HasIntegral } I\ l\ (\lambda x. 0)\ vol\ 0$$$

Lean4

theorem hasIntegral_zero : HasIntegral I l (fun _ => (0 : E)) vol 0 := by
  simpa only [← (vol I).map_zero] using hasIntegral_const (0 : E)

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

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

Разделы

Аффилиация

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