toZeroAtInftyCLM_apply

Mathlib.Analysis.Distribution.SchwartzSpace

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

English

The zero-at-infinity CLM acts pointwise by evaluation, i.e., (toZeroAtInftyCLM f)(x) = f(x).

Русский

CLM-применение действует по точкам: (toZeroAtInftyCLM f)(x) = f(x).

LaTeX

$$$$ (toZeroAtInftyCLM)\\, f\\, x = f(x). $$$$

Lean4

@[simp]
theorem toZeroAtInftyCLM_apply (f : 𝓢(E, F)) (x : E) : toZeroAtInftyCLM 𝕜 E F f x = f x :=
  rfl

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

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

Разделы

Аффилиация

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