English
If f has compact multiplicative support, f₂ has compact multiplicative support, and m 1 1 = 1, then the function x ↦ m (f x) (f₂ x) has compact multiplicative support.
Русский
Если mulTSupport(f) и mulTSupport(f₂) компактны и m 1 1 = 1, то функция x ↦ m(f x)(f₂ x) имеет компактную мультиподдержку.
LaTeX
$$$\\text{HasCompactMulSupport}(f) \\land \\text{HasCompactMulSupport}(f₂) \\land (m\\,1\\,1 = 1) \\Rightarrow \\text{HasCompactMulSupport}(\\lambda x, m (f x) (f₂ x)).$$$
Lean4
@[to_additive]
theorem comp₂_left (hf : HasCompactMulSupport f) (hf₂ : HasCompactMulSupport f₂) (hm : m 1 1 = 1) :
HasCompactMulSupport fun x => m (f x) (f₂ x) :=
by
rw [hasCompactMulSupport_iff_eventuallyEq] at hf hf₂ ⊢
filter_upwards [hf, hf₂] with x hx hx₂
simp_rw [hx, hx₂, Pi.one_apply, hm]
