sum_cond

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

Sum over a conditional family equals the sum of the two branches: sum (λ b, cond b μ ν) = μ + ν.

Русский

Сумма по условной семье равна сумме двух ветвей: sum (λ b, cond b μ ν) = μ + ν.

LaTeX

$$$ \sum_{b} (\text{cond } b\; μ\; ν) = μ + ν $$$

Lean4

theorem sum_cond (μ ν : Measure α) : (sum fun b => cond b μ ν) = μ + ν :=
  sum_bool _

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

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

Разделы

Аффилиация

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