instSMulOfContinuousConstSMul — Mathlib

English

If β has a scalar action by R that is continuous, then there is a natural SMul R-action on C_c(α,β) defined pointwise by (r•f)(x) = r•(f(x)) and preserving compact support.

Русский

Пусть β имеет скалярное действие от R, непрерывное; тогда C_c(α,β) наследует действие SMul от R, задаваемое по точкам: (r•f)(x) = r•(f(x)), и сохраняет компактную опору.

LaTeX

$$$$(r\cdot f)(x) = r\cdot f(x) \quad \text{for all } r\in R, f\in C_c(\alpha,\beta), x\in \alpha.$$$$

Lean4

instance [Zero β] {R : Type*} [SMulZeroClass R β] [ContinuousConstSMul R β] : SMul R C_c(α, β) :=
  ⟨fun r f => ⟨⟨r • ⇑f, (map_continuous f).const_smul r⟩, HasCompactSupport.smul_left f.2⟩⟩

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