instContinuousSMul — Mathlib

English

SchwartzMap is a continuous module over 𝕜: scalar multiplication is continuous with respect to the Schwartz-space topology.

Русский

SchwartzMap является непрерывным модулем над 𝕜: скалярное умножение непрерывно в топологии Schwartz-пространства.

LaTeX

$$$\mathrm{instContinuousSMul}: \text{ContinuousSMul } 𝕜\; \mathcal{S}(E,F)$$$

Lean4

instance instContinuousSMul : ContinuousSMul 𝕜 𝓢(E, F) :=
  by
  rw [(schwartz_withSeminorms 𝕜 E F).withSeminorms_eq]
  exact (schwartzSeminormFamily 𝕜 E F).moduleFilterBasis.continuousSMul

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