smulc_apply — Mathlib

English

The pointwise scalar action on C_c(α, β) respects evaluation: (f • g)(x) = f(x) • g(x).

Русский

Пошаговое скалярное действие на C_c(α, β) сохраняет значение: (f • g)(x) = f(x) • g(x).

LaTeX

$$$ (f • g) x = f(x) \cdot g(x) $$$

Lean4

theorem smulc_apply [Zero β] [TopologicalSpace γ] [SMulZeroClass γ β] [ContinuousSMul γ β] {F : Type*} [FunLike F α γ]
    [ContinuousMapClass F α γ] (f : F) (g : C_c(α, β)) (x : α) : (f • g) x = f x • g x :=
  rfl

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