sum_bool

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

If the index is Bool, then sum μ equals μ_true plus μ_false.

Русский

Если индекс — Bool, то сумма μ равна μ_true + μ_false.

LaTeX

$$$ \sum_{b\in\text{Bool}} μ_b = μ_{\text{true}} + μ_{\text{false}} $$$

Lean4

theorem sum_bool (f : Bool → Measure α) : sum f = f true + f false := by rw [sum_fintype, Fintype.sum_bool]

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

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

Разделы

Аффилиация

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