English
If TendstoUniformlyOnFilter F f p p' holds and F and F' agree on the argument on a set s eventually, then TendstoUniformlyOnFilter F' f p p' holds.
Русский
Если имеется сходимость по равномерности для фильтра и F и F' совпадают на наборе, то F' сохраняет это свойство.
LaTeX
$$$\\ TendstoUniformlyOnFilter F f p p' \\land (\\forall^\\! n \\in p, \\text{EqOn}(F n, F' n) s) \\Rightarrow TendstoUniformlyOnFilter F' f p p'$$$
Lean4
theorem congr {F' : ι → α → β} (hf : TendstoUniformlyOn F f p s) (hff' : ∀ᶠ n in p, Set.EqOn (F n) (F' n) s) :
TendstoUniformlyOn F' f p s :=
by
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at hf ⊢
refine hf.congr ?_
rw [eventually_iff] at hff' ⊢
simp only [Set.EqOn] at hff'
simp only [mem_prod_principal, hff', mem_setOf_eq]
