coe_add — Mathlib

English

Let μ1 and μ2 be measures on a measurable space. For every measurable set s, the sum measure satisfies (μ1 + μ2)(s) = μ1(s) + μ2(s). In particular the value of the sum on a set is the sum of the individual values.

Русский

Пусть μ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

@[simp, norm_cast]
theorem coe_add {_m : MeasurableSpace α} (μ₁ μ₂ : Measure α) : ⇑(μ₁ + μ₂) = μ₁ + μ₂ :=
  rfl

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