coeFn_zero

Mathlib.Analysis.Distribution.SchwartzSpace

URI: https://scilib.ai/kg/mathlib#SchwartzMap.coeFn_zero

English

The function corresponding to the zero map is the zero function.

Русский

Функция, соответствующая нулевой карте, равна нулевой функции.

LaTeX

$$$ \\mathrm{coeff}(0) = 0 \\, (\\text{as a function})$$$

Lean4

@[simp]
theorem coeFn_zero : ⇑(0 : 𝓢(E, F)) = (0 : E → F) :=
  rfl

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

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

Разделы

Аффилиация

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