integrableOn_univ

Mathlib.MeasureTheory.Integral.IntegrableOn

URI: https://scilib.ai/kg/mathlib#MeasureTheory.integrableOn_univ

English

Integrable on the universe set corresponds to integrable on μ.

Русский

Интегрируемость на весь простор эквивалентна интегрируемости по мере μ.

LaTeX

$$$ \text{IntegrableOn}(f,\mathsf{univ},\mu) \;\Leftrightarrow\; \text{Integrable}(f,\mu) $$$

Lean4

@[simp]
theorem integrableOn_univ : IntegrableOn f univ μ ↔ Integrable f μ := by rw [IntegrableOn, Measure.restrict_univ]

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

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

Разделы

Аффилиация

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