toZeroAtInfty_toBCF

Mathlib.Analysis.Distribution.SchwartzSpace

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

English

The zero-at-infinity realization and the BCFunction realization coincide for Schwartz maps.

Русский

Реализации нулевого поведения в бесконечности и BCFunction совпадают для отображений Шварца.

LaTeX

$$$$ f^{\\mathrm{toZI}} = f^{\\mathrm{toBCF}}. $$$$

Lean4

@[simp]
theorem toZeroAtInfty_toBCF (f : 𝓢(E, F)) : f.toZeroAtInfty.toBCF = f.toBoundedContinuousFunction :=
  rfl

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

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

Разделы

Аффилиация

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