mono_measure

Mathlib.MeasureTheory.Integral.IntegrableOn

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

English

If f is integrable on s with respect to ν, and μ ≤ ν, then f is integrable on s with respect to μ.

Русский

Если f интегрируема на s по ν, и μ ≤ ν, то f интегрируема на s по μ.

LaTeX

$$$\mathrm{IntegrableOn}(f,s,\nu) \to \mu \le \nu \to \mathrm{IntegrableOn}(f,s,\mu)$$$

Lean4

theorem mono_measure (h : IntegrableOn f s ν) (hμ : μ ≤ ν) : IntegrableOn f s μ :=
  h.mono (Subset.refl _) hμ

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

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

Разделы

Аффилиация

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