instIsScalarTowerOfReal — Mathlib

English

The SMul instance on seminorms is given by extending the existing seminorm with a scaled function, preserving linearity and scalar compatibility.

Русский

Инстанс SMul на семинорме задаётся расширением существующей семинормы до масштаба функции, сохраняя линейность и совместимость со скалярами.

LaTeX

$$$\text{instSMul}$ defined as above$$

Lean4

instance [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] [SMul R' ℝ] [SMul R' ℝ≥0] [IsScalarTower R' ℝ≥0 ℝ] [SMul R R']
    [IsScalarTower R R' ℝ] : IsScalarTower R R' (Seminorm 𝕜 E) where
  smul_assoc r a p := ext fun x => smul_assoc r a (p x)

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