right_of_union

Mathlib.MeasureTheory.Integral.IntegrableOn

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

English

If f is integrable on s ∪ t with respect to μ, then it is integrable on t with μ.

Русский

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

LaTeX

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

Lean4

theorem right_of_union (h : IntegrableOn f (s ∪ t) μ) : IntegrableOn f t μ :=
  h.mono_set subset_union_right

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

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

Разделы

Аффилиация

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