English
The space of compactly supported bounded continuous functions is closed under multiplication by continuous functions pointwise: for g ∈ C(α, γ) and f ∈ compactlySupported α γ, the product g · f has compact support.
Русский
Пространство компактно поддерживаемых ограниченно непрерывных функций замкнуто относительно умножения на непрерывные функции по определению: если g ∈ C(α, γ) и f ∈ compactlySupported α γ, то g·f имеет компактную опору.
LaTeX
$$HasCompactSupport (instHMul.hMul (ContinuousMap.instFunLike.coe g) (BoundedContinuousFunction.instFunLike.coe f.val))$$
Lean4
instance : SMul C(α, γ) C_cb(α, γ) where
smul := fun (g : C(α, γ)) =>
(fun (f : C_cb(α, γ)) =>
⟨ofCompactSupport (g * (f : α →ᵇ γ) : α → γ) (Continuous.mul g.2 f.1.1.2)
(HasCompactSupport.mul_left (mem_compactlySupported.mp f.2)),
by
apply mem_compactlySupported.mpr
rw [ofCompactSupport]
exact HasCompactSupport.mul_left <| mem_compactlySupported.mp f.2⟩)
