English
If f =^l f' and g =^l g', then for any binary operation h, (f x, g x) =^l (f' x, g' x).
Русский
Если f =^l f' и g =^l g', то для любой бинарной операции h выполняется, что h(f,g) =^l h(f',g').
LaTeX
$$$\\\\forall f,f' : \\\\alpha \\\\to \\\\beta, \\\\forall g,g' : \\\\alpha \\\\to \\\\gamma, \\\\forall l \\\\ (l : Filter \\\\alpha), \\\\ (f =^l f') \\\\Rightarrow \\\\ (g =^l g') \\\\Rightarrow \\\\bigl((\\\\lambda x. h (f x) (g x)) =^l (\\\\lambda x. h (f' x) (g' x))\\\\bigr)$$$$
Lean4
theorem comp₂ {δ} {f f' : α → β} {g g' : α → γ} {l} (Hf : f =ᶠ[l] f') (h : β → γ → δ) (Hg : g =ᶠ[l] g') :
(fun x => h (f x) (g x)) =ᶠ[l] fun x => h (f' x) (g' x) :=
(Hf.prodMk Hg).fun_comp (uncurry h)
