intervalIntegrable_sin

Mathlib.Analysis.SpecialFunctions.Integrability.Basic

URI: https://scilib.ai/kg/mathlib#intervalIntegral.intervalIntegrable_sin

English

The sine function is interval-integrable on any finite interval.

Русский

Синус-функция интегрируема по любому конечному интервалу.

LaTeX

$$$\text{IntervalIntegrable } \sin$ на любом интервале$$

Lean4

@[simp]
theorem intervalIntegrable_sin : IntervalIntegrable sin μ a b :=
  continuous_sin.intervalIntegrable a b

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

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

Разделы

Аффилиация

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