torusIntegrable_const

Mathlib.MeasureTheory.Integral.TorusIntegral

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

← MathLib Explorer

English

Constant functions are torus integrable for any c and R.

Русский

Постоянные функции интегрируемы на торусе для любых c и R.

LaTeX

$$$\\mathrm{TorusIntegrable}(\\lambda\\_x a, c, R)\\equiv \\text{true}$$$

Lean4

/-- Constant functions are torus integrable -/
theorem torusIntegrable_const (a : E) (c : ℂⁿ) (R : ℝⁿ) : TorusIntegrable (fun _ => a) c R := by
  simp [TorusIntegrable, measure_Icc_lt_top]

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

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

Разделы

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

Аффилиация

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