comp_add

Mathlib.Probability.Kernel.Composition.MeasureComp

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

← MathLib Explorer

English

κ ∘ₘ (μ + ν) = (κ ∘ₘ μ) + (κ ∘ₘ ν).

Русский

Композиция κ с суммой мер μ + ν равняется сумме κ ∘ μ и κ ∘ ν.

LaTeX

$$$\\kappa \\circ_{m} (\\mu + \\nu) = (\\kappa \\circ_{m} \\mu) + (\\kappa \\circ_{m} \\nu)$$$

Lean4

@[simp]
theorem comp_add : κ ∘ₘ (μ + ν) = κ ∘ₘ μ + κ ∘ₘ ν := by
  simp_rw [comp_eq_comp_const_apply, Kernel.const_add, Kernel.comp_add_right, Kernel.add_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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