coe_add

Mathlib.Topology.ContinuousMap.ContinuousMapZero

URI: https://scilib.ai/kg/mathlib#ContinuousMapZero.coe_add

English

The coercion respects addition: the underlying function of f+g equals the sum of the underlying functions.

Русский

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

LaTeX

$$toFun(f+g) = toFun(f) + toFun(g)$$

Lean4

@[simp]
theorem coe_add [AddZeroClass R] [ContinuousAdd R] (f g : C(X, R)₀) : ⇑(f + g) = f + g :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru