left_of_union

Mathlib.MeasureTheory.Integral.IntegrableOn

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

English

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

Русский

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

LaTeX

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

Lean4

theorem left_of_union (h : IntegrableOn f (s ∪ t) μ) : IntegrableOn f s μ :=
  h.mono_set subset_union_left

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

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

Разделы

Аффилиация

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