coeFnAddMonoidHom — Mathlib

English

For a finite index set ι and a finite family of zero-preserving continuous maps f_i, the canonical coefficient sum satisfies the natural equation: the underlying function of the sum equals the sum of underlying functions.

Русский

Для конечного множества индексов ι и конечной семьи отображений f_i из C(X,R)₀, имеющих нулевой предел, естественно верно, что функция-образ суммы равна сумме функций-образов.

LaTeX

$$$\\text{coe\_sum } (s : Finset ι) (f : ι \\to C(X,R)₀) : \\Rightarrow \\text{coe}(s.sum f) = s.sum (fun i => (coe (f i)))$$$

Lean4

/-- Coercion to a function as an `AddMonoidHom`. Similar to `ContinuousMap.coeFnAddMonoidHom`. -/
def coeFnAddMonoidHom : C(X, R)₀ →+ X → R where
  toFun f := f
  map_zero' := coe_zero
  map_add' f g := by simp

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