English
If f =^l f' and g =^l g' along a filter l, then the pair (f,g) is eventually equal to the pair (f',g').
Русский
Если пары функций совпадают порознь по фильтру l, то соответствующая пара функций совпадает поровну по фильтру l.
LaTeX
$$$\\\\forall l \\\\ (l : Filter \\\\alpha), \\\\forall f,f' : \\\\alpha \\\\to \\\\beta, \\\\forall g,g' : \\\\alpha \\\\to \\\\gamma, \\\\ (f =^l f') \\\\Rightarrow \\\\ (g =^l g') \\\\Rightarrow \\\\bigl((\\\\lambda x. (f x, g x)) =^l (\\\\lambda x. (f' x, g' x))\\\\bigr)$$$
Lean4
theorem prodMk {l} {f f' : α → β} (hf : f =ᶠ[l] f') {g g' : α → γ} (hg : g =ᶠ[l] g') :
(fun x => (f x, g x)) =ᶠ[l] fun x => (f' x, g' x) :=
hf.mp <|
hg.mono <| by
intros
simp only [*]
