le_sum_apply

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.le_sum_apply

English

For any family f: ι → Measure α and any set s, sum f i s ≤ sum f s.

Русский

Для любой функции f: ι → Measure α и любого множества s, ∑' i, f i s ≤ sum f s.

LaTeX

$$$ \\sum_{i} f(i)(s) \\le \\sum f(s) $$$$

Lean4

theorem le_sum_apply (f : ι → Measure α) (s : Set α) : ∑' i, f i s ≤ sum f s :=
  le_toMeasure_apply _ _ _

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

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

Разделы

Аффилиация

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