instAdd

Mathlib.Topology.ContinuousMap.ZeroAtInfty

URI: https://scilib.ai/kg/mathlib#ZeroAtInftyContinuousMap.instAdd

← MathLib Explorer

English

C₀(α, β) carries an addition defined pointwise: (f+g)(x) = f(x) + g(x).

Русский

C₀(α, β) имеет сложение, определяемое по точкам: (f+g)(x) = f(x) + g(x).

LaTeX

$$$ (f + g)(x) = f(x) + g(x) $$$

Lean4

instance instAdd [AddZeroClass β] [ContinuousAdd β] : Add C₀(α, β) :=
  ⟨fun f g => ⟨f + g, by simpa only [add_zero] using (zero_at_infty f).add (zero_at_infty g)⟩⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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