English
If two families F and F' of α → β are eventually equal along a filter p (i.e., F =ᶠ[p] F'), then F f converges uniformly to f with respect to p if and only if F' f converges uniformly to f with respect to p.
Русский
Если две семейства F и F' функций α → β совпадают точно на хвосте фильтра p (F =ᶠ[p] F'), то F f сходится равномерно к f по p тогда и только тогда, когда F' f сходится равномерно к f по p.
LaTeX
$$$(F =^\!{p} F') \Rightarrow (\text{TendstoUniformly } F\ f\ p \iff \text{TendstoUniformly } F'\ f\ p)$$$
Lean4
theorem tendstoUniformly_congr {F' : ι → α → β} (hF : F =ᶠ[p] F') : TendstoUniformly F f p ↔ TendstoUniformly F' f p :=
by
simp_rw [← tendstoUniformlyOn_univ] at *
have HF := EventuallyEq.exists_mem hF
exact ⟨fun h => h.congr (by aesop), fun h => h.congr (by simp_rw [eqOn_comm]; aesop)⟩
