schwartzSeminormFamily — Mathlib

English

The module structure on SchwartzMap is compatible with the underlying coercion to functions, via a standard lemma about modules over 𝕜.

Русский

Структура модуля на SchwartzMap согласована с переводом в функции через стандартную лемму про модули над 𝕜.

LaTeX

$$$\mathrm{instModule} : Module 𝕜 \mathcal{S}(E,F)$$$

Lean4

/-- The family of Schwartz seminorms. -/
def _root_.schwartzSeminormFamily : SeminormFamily 𝕜 𝓢(E, F) (ℕ × ℕ) := fun m => SchwartzMap.seminorm 𝕜 m.1 m.2

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