instMul — Mathlib

English

The product of two vanishing-at-infinity maps f and g is the map defined by (f*g)(x) = f(x) g(x).

Русский

Произведение двух отображений, исчезающих в бесконечности, задаётся точечно: (f*g)(x) = f(x) g(x).

LaTeX

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

Lean4

instance instMul [MulZeroClass β] [ContinuousMul β] : Mul C₀(α, β) :=
  ⟨fun f g => ⟨f * g, by simpa only [mul_zero] using (zero_at_infty f).mul (zero_at_infty g)⟩⟩

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