enorm

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

English

The norm of an interval integrable function is interval integrable as well.

Русский

Норма интервально интегрируемой функции тоже интервально интегрируема.

LaTeX

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

Lean4

theorem enorm (h : IntervalIntegrable f μ a b) : IntervalIntegrable (‖f ·‖ₑ) μ a b :=
  ⟨h.1.enorm, h.2.enorm⟩

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

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

Разделы

Аффилиация

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