continuous

Mathlib.Analysis.Distribution.SchwartzSpace

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

English

Every Schwartz map is differentiable of all orders.

Русский

Каждое Schwartz-отображение дифференцируемо во всех порядках.

LaTeX

$$$ \text{SchwartzMap.differentiable}: \forall f \in \mathcal{S}(E,F), \text{ (D^n f) exists for all n} $$$

Lean4

/-- Every Schwartz function is continuous. -/
@[continuity]
protected theorem continuous (f : 𝓢(E, F)) : Continuous f :=
  (f.smooth 0).continuous

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

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

Разделы

Аффилиация

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