const_add

Mathlib.Probability.Kernel.Basic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.const_add

English

Const β preserves addition: const β (μ+ν) = const β μ + const β ν.

Русский

Const β сохраняет сложение: const β (μ+ν) = const β μ + const β ν.

LaTeX

$$$\text{const}_β(\mu + \nu) = \text{const}_β(\mu) + \text{const}_β(\nu)$$$

Lean4

theorem const_add (β : Type*) [MeasurableSpace β] (μ ν : Measure α) : const β (μ + ν) = const β μ + const β ν := by ext;
  simp

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

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

Разделы

Аффилиация

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