coeFn_add — Mathlib

English

Let μ and ν be finite measures on Ω. Then the value of their sum on any set equals the sum of their values on that set: (μ + ν)(A) = μ(A) + ν(A).

Русский

Пусть μ и ν — конечные меры на Ω. Тогда значение их суммы на произвольном множестве A равно сумме значений этих мер на A: (μ + ν)(A) = μ(A) + ν(A).

LaTeX

$$$\forall A \subseteq \Omega,\ (\mu + \nu)(A) = \mu(A) + \nu(A)$$$

Lean4

@[simp, norm_cast]
theorem coeFn_add (μ ν : FiniteMeasure Ω) : (⇑(μ + ν) : Set Ω → ℝ≥0) = (⇑μ + ⇑ν : Set Ω → ℝ≥0) :=
  by
  funext
  simp only [Pi.add_apply, ← ENNReal.coe_inj, ennreal_coeFn_eq_coeFn_toMeasure, ENNReal.coe_add]
  norm_cast

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