torusIntegrable_zero_radius

Mathlib.MeasureTheory.Integral.TorusIntegral

URI: https://scilib.ai/kg/mathlib#TorusIntegrable.torusIntegrable_zero_radius

← MathLib Explorer

English

For any f and c, TorusIntegrable f c 0 holds.

Русский

Для любого f и любого c справедливо, что TorusIntegrable f c 0.

LaTeX

$$$\forall f,c,\ \operatorname{TorusIntegrable}(f,c,0)$$$

Lean4

theorem torusIntegrable_zero_radius {f : (ℂⁿ) → E} {c : ℂⁿ} : TorusIntegrable f c 0 :=
  by
  rw [TorusIntegrable, torusMap_zero_radius]
  apply torusIntegrable_const (f c) c 0

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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