mul — Mathlib

English

The product of two HasCompactMulSupport functions has HasCompactMulSupport.

Русский

Произведение двух функций с компактной мультиподдержкой также имеет компактную мультиподдержку.

LaTeX

$$$\\text{HasCompactMulSupport}(f) \\land \\text{HasCompactMulSupport}(f') \\Rightarrow \\text{HasCompactMulSupport}(f\\cdot f').$$$

Lean4

@[to_additive]
theorem mul (hf : HasCompactMulSupport f) (hf' : HasCompactMulSupport f') : HasCompactMulSupport (f * f') :=
  hf.comp₂_left hf' (mul_one 1)

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