English
If TendstoUniformlyOn F f p s holds and F and F' coincide on s eventually (in p), then TendstoUniformlyOn F' f p s holds.
Русский
Если F сходится равномерно на s и F и F' совпадают на s почти наверняка по p, то F' также сходится на s.
LaTeX
$$$\\ TendstoUniformlyOn F f p s \\land (\\forall^\\! n in p, \\text{EqOn}(F n) (F' n) s) \\Rightarrow TendstoUniformlyOn F' f p s$$$
Lean4
theorem prodMap {ι' α' β' : Type*} [UniformSpace β'] {F' : ι' → α' → β'} {p' : Filter ι'} {s' : Set α'}
(h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p' s') :
UniformCauchySeqOn (fun i : ι × ι' => Prod.map (F i.1) (F' i.2)) (p ×ˢ p') (s ×ˢ s') :=
by
intro u hu
rw [uniformity_prod_eq_prod, mem_map, mem_prod_iff] at hu
obtain ⟨v, hv, w, hw, hvw⟩ := hu
simp_rw [mem_prod, and_imp, Prod.forall, Prod.map_apply]
rw [← Set.image_subset_iff] at hvw
apply (tendsto_swap4_prod.eventually ((h v hv).prod_mk (h' w hw))).mono
intro x hx a b ha hb
exact hvw ⟨_, mk_mem_prod (hx.1 a ha) (hx.2 b hb), rfl⟩
