mono_set

Mathlib.MeasureTheory.Integral.IntegrableOn

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

English

If f is integrable on t with respect to μ and s ⊆ t, then f is integrable on s with the same μ.

Русский

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

LaTeX

$$$\mathrm{IntegrableOn}(f,t,\mu) \to s \subseteq t \to \mathrm{IntegrableOn}(f,s,\mu)$$$

Lean4

theorem mono_set (h : IntegrableOn f t μ) (hst : s ⊆ t) : IntegrableOn f s μ :=
  h.mono hst le_rfl

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

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

Разделы

Аффилиация

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