sum_apply — Mathlib

English

For a family f : ι → OuterMeasure α, the sum measure satisfies sum f on s equals the sum of f_i on s: sum f s = ∑' i, f_i s.

Русский

Для семейства f : ι → OuterMeasure α сумма оказывается на множествах как сумма значений f_i на s: sum f s = ∑' i, f_i s.

LaTeX

$$$ sum\ f\ s = \sum_{i} f(i)(s) $$$

Lean4

@[simp]
theorem sum_apply {ι} (f : ι → OuterMeasure α) (s : Set α) : sum f s = ∑' i, f i s :=
  rfl

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