mul_left — Mathlib

English

If f' has compact support, then the pointwise product f · f' also has compact support.

Русский

Если f' имеет компактную опору, то поэлементное произведение f · f' тоже имеет компактную опору.

LaTeX

$$$\operatorname{HasCompactSupport}(f') \Rightarrow \operatorname{HasCompactSupport}(f \cdot f').$$$

Lean4

theorem mul_left (hf : HasCompactSupport f') : HasCompactSupport (f * f') :=
  by
  rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
  exact hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]

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