of_measure_zero

Mathlib.MeasureTheory.Integral.IntegrableOn

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IntegrableOn.of_measure_zero

English

Let μ be a measure on α and s ⊆ α. If μ(s) = 0, then f is integrable on s with respect to μ.

Русский

Пусть μ — мера на пространства α и s ⊆ α. Если μ(s) = 0, то f интегрируема на s по μ.

LaTeX

$$$\mu(s) = 0 \Rightarrow \mathrm{IntegrableOn}(f,s,\mu)$$$

Lean4

theorem of_measure_zero (hs : μ s = 0) : IntegrableOn f s μ := by simp [IntegrableOn, Measure.restrict_eq_zero.2 hs]

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

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

Разделы

Аффилиация

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