English
Let l be a filter on a space X, and for a finite index set s ⊆ ι consider functions f_i, g_i : X → M into a commutative monoid M with continuous multiplication. If for every i in s we have f_i =ᶠ[l] g_i, then the products over i ∈ s are also eventually equal: ∏_{i∈s} f_i =ᶠ[l] ∏_{i∈s} g_i (as functions X → M).
Русский
Пусть l — фильтр на пространстве X. Пусть для конечного множества индексов s ⊆ ι даны функции f_i, g_i : X → M в коммутативном моноиде M с непрерывным умножением. Если для каждого i ∈ s выполнено f_i =ᶠ[l] g_i, то и произведения по i ∈ s совпадают локально: ∏_{i∈s} f_i =ᶠ[l] ∏_{i∈s} g_i (как функции X → M).
LaTeX
$$$\\exists s : \\mathrm{Finset}\\,\\iota,\\, l.\\mathrm{EventuallyEq}\\left(\\lambda x \\mapsto \\prod_{i \\in s} f_i(x)\\right)\\left(\\lambda x \\mapsto \\prod_{i \\in s} g_i(x)\\right)$$$
Lean4
@[to_additive]
theorem eventuallyEq_prod {X M : Type*} [CommMonoid M] {s : Finset ι} {l : Filter X} {f g : ι → X → M}
(hs : ∀ i ∈ s, f i =ᶠ[l] g i) : ∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i :=
by
replace hs : ∀ᶠ x in l, ∀ i ∈ s, f i x = g i x := by rwa [eventually_all_finset]
filter_upwards [hs] with x hx
simp only [Finset.prod_apply, Finset.prod_congr rfl hx]
