zero

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

URI: https://scilib.ai/kg/mathlib#IntervalIntegrable.zero

English

If f is interval integrable, then the function taking norms is interval integrable as well.

Русский

Если f интервально интегрируема, то функция норм по ней тоже интервально интегрируема.

LaTeX

$$$$\text{IntervalIntegrable}(\|f\|, μ, a, b).$$$$

Lean4

protected theorem zero : IntervalIntegrable (0 : ℝ → E) μ a b :=
  (intervalIntegrable_const_iff <| by finiteness).mpr <| .inl rfl

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

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

Разделы

Аффилиация

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