coe_sum — Mathlib

English

The coercion of a finite sum of bounded continuous functions equals the finite sum of their coercions: coe_sum s f = ∑ i∈s coe(f_i).

Русский

Преобразование конечной суммы ограниченных непрерывных функций эквивалентно конечной сумме их коэрций: coe_sum s f = ∑ i∈s coe(f_i).

LaTeX

$$$\operatorname{coe}(\sum_{i\in s} f_i) = \sum_{i\in s} \operatorname{coe}(f_i)$$$

Lean4

@[simp]
theorem coe_sum {ι : Type*} (s : Finset ι) (f : ι → α →ᵇ β) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, (f i : α → β) :=
  map_sum coeFnAddHom f s

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