mul_apply — Mathlib

English

C₀(α, β) inherits a SemigroupWithZero structure with pointwise multiplication and zero as the neutral element at infinity.

Русский

C₀(α, β) наследует структуру SemigroupWithZero: умножение по точкам и нуль в качестве нулевого элемента на бесконечности.

LaTeX

$$$ (f * g)(x) = f(x) g(x) \quad \text{and} \quad 0(x) = 0 $$$

Lean4

theorem mul_apply [MulZeroClass β] [ContinuousMul β] (f g : C₀(α, β)) : (f * g) x = f x * g x :=
  rfl

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