toReal_add

Mathlib.Topology.ContinuousMap.CompactlySupported

URI: https://scilib.ai/kg/mathlib#CompactlySupportedContinuousMap.toReal_add

English

The toReal map preserves addition: the real realization of a sum equals the sum of the realizations.

Русский

Преобразование toReal сохраняет сложение: toReal(f+g) = toReal(f) + toReal(g).

LaTeX

$$$ (f + g)^{\\mathrm{toReal}} = f^{\\mathrm{toReal}} + g^{\\mathrm{toReal}}. $$$

Lean4

@[simp]
theorem toReal_add (f g : C_c(α, ℝ≥0)) : (f + g).toReal = f.toReal + g.toReal := by ext; simp

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

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

Разделы

Аффилиация

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