instSMulOfContinuousSMulOfContinuousMapClass

English

There is a natural action of F on C_c(α, β) given by (f • g)(x) = f(x) • g(x) when F is a FunLike α→γ with ContinuousMapClass α→γ and β is a Manifold-like type with ContinuousSMul.

Русский

Существует естественное действие F на C_c(α, β): (f • g)(x) = f(x) • g(x) при условиях.

LaTeX

$$$ SMul F C_c(α, β) \;:\; smul\ f\ g := ⟨⟨fun x ↦ f x • g x, \dots⟩, g.hasCompactSupport.smul_left⟩ $$$

Lean4

/-- the product of `f : F` assuming `ContinuousMapClass F α γ` and `ContinuousSMul γ β` and
`g : C_c(α, β)` is in `C_c(α, β)` -/
instance [Zero β] [TopologicalSpace γ] [SMulZeroClass γ β] [ContinuousSMul γ β] {F : Type*} [FunLike F α γ]
    [ContinuousMapClass F α γ] : SMul F C_c(α, β) where
  smul f g := ⟨⟨fun x ↦ f x • g x, (map_continuous f).smul (map_continuous g)⟩, g.hasCompactSupport.smul_left⟩

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