mul_right — Mathlib

English

The product f * f' has compact support if both f and f' have compact support.

Русский

Произведение f и f' имеет компактную опору, если обе имеют компактную опору.

LaTeX

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

Lean4

theorem mul_right (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, zero_mul]

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