English
If HasProdUniformlyOn f g 𝔖 holds and f and f' are pointwise equivalent on every s∈𝔖 (i.e., f i ≡ f' i on s for all i), then HasProdUniformlyOn f' g 𝔖 holds as well.
Русский
Если HasProdUniformlyOn f g 𝔖 выполняется и для всех i функция f i совпадает с f' i на каждом s∈𝔖 (наборы равны), то HasProdUniformlyOn f' g 𝔖 тоже выполняется.
LaTeX
$$$ HasProdUniformlyOn\ f\ g\ 𝔖 \to (\forall i, s\in 𝔖, f_i\equiv_s f'_i) \Rightarrow HasProdUniformlyOn\ f'\ g\ 𝔖 $$$
Lean4
@[to_additive]
theorem congr {f' : ι → β → α} (h : HasProdUniformlyOn f g 𝔖)
(hff' : ∀ s ∈ 𝔖, ∀ᶠ (n : Finset ι) in atTop, Set.EqOn (fun b ↦ ∏ i ∈ n, f i b) (fun b ↦ ∏ i ∈ n, f' i b) s) :
HasProdUniformlyOn f' g 𝔖 := by
rw [hasProdUniformlyOn_iff_tendstoUniformlyOn] at *
exact fun s hs ↦ TendstoUniformlyOn.congr (h s hs) (hff' s hs)
