coe_add — Mathlib

English

The canonical coercion of the sum equals the sum of the coerces: the underlying function of f+g is the sum of the underlying functions.

Русский

Каноническое вложение суммы равно сумме вложений: базовая функция f+g равна сумме функций f и g.

LaTeX

$$$\\big( f+g \\big) \\text{ as a function} = (f \\text{ as a function}) + (g \\text{ as a function})$$$

Lean4

@[simp, norm_cast]
theorem coe_add (f g : CauSeq β abv) : ⇑(f + g) = (f : ℕ → β) + g :=
  rfl

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