coe_finset_sum — Mathlib

English

Finite sums of measures respect the coercion: the coercion commutes with Finset sums: coe_finset_sum I μ = ∑ i∈I, coe(μ_i).

Русский

Конечные суммы мер сохраняют отображение: коэрцирование суммируется через Finset.

LaTeX

$$$\forall I:\ text{Finset }\iota, \; (\sum i \in I, μ_i)^{\text{coe}} = \sum i \in I, μ_i^{\text{coe}}$$$

Lean4

@[simp]
theorem coe_finset_sum {_m : MeasurableSpace α} (I : Finset ι) (μ : ι → Measure α) :
    ⇑(∑ i ∈ I, μ i) = ∑ i ∈ I, ⇑(μ i) :=
  map_sum coeAddHom μ I

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