English
If f =^l f' and g =^l g', then f · g =^l f' · g' under SMul structure.
Русский
Если f =^l f' и g =^l g', то f · g =^l f' · g' при заданной структуре SMul.
LaTeX
$$$\\\\forall 𝕜 \\\\ [SMul 𝕜 β], \\\\forall l \\\\ (l : Filter \\\\alpha), \\\\forall f,f' : \\\\alpha \\\\to \\\\mathbb{𝕜}, \\\\forall g,g' : \\\\alpha \\\\to β, \\\\ (f =^l f') \\\\Rightarrow \\\\ (g =^l g') \\\\Rightarrow \\\\bigl((\\\\lambda x. f(x) \\• g(x)) =^l (\\\\lambda x. f'(x) \\• g'(x))\\\\bigr)$$$
Lean4
@[to_additive]
theorem smul {𝕜} [SMul 𝕜 β] {l : Filter α} {f f' : α → 𝕜} {g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
(fun x => f x • g x) =ᶠ[l] fun x => f' x • g' x :=
hf.comp₂ (· • ·) hg
