instContinuousMapClass

Mathlib.Analysis.Distribution.SchwartzSpace

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

English

Schwartz maps form aContinuousMapClass with continuous maps by definition.

Русский

Отображения Шварца образуют continuous map class по определению.

LaTeX

$$$ \text{SchwartzMap.instContinuousMapClass} : ContinuousMapClass 𝓢(E,F) E F $$$

Lean4

instance instContinuousMapClass : ContinuousMapClass 𝓢(E, F) E F where map_continuous := SchwartzMap.continuous

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

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

Разделы

Аффилиация

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