add_apply

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

For any measures μ1, μ2 and any set s, (μ1 + μ2)(s) = μ1(s) + μ2(s).

Русский

Для любых мер μ1, μ2 и множества s выполняется (μ1 + μ2)(s) = μ1(s) + μ2(s).

LaTeX

$$$\forall \mu_1,\mu_2: \text{Measure}(\alpha),\; \forall s: Set(\alpha),\; (\mu_1 + \mu_2)(s) = \mu_1(s) + \mu_2(s).$$$

Lean4

theorem add_apply {_m : MeasurableSpace α} (μ₁ μ₂ : Measure α) (s : Set α) : (μ₁ + μ₂) s = μ₁ s + μ₂ s :=
  rfl

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

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

Разделы

Аффилиация

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