English
If a sequence g converges to b in the ambient space, then TendstoUniformlyOn F (constant function b) p s is equivalent to TendstoUniformlyOn F (fun n => g(n)) p s.
Русский
Если g сходится к b во внешнем пространстве, то равномерная сходимость F к константе b на p и s эквивалентна TendstoUniformlyOn F g.
LaTeX
$$TendstoUniformlyOnConst : (hg : Tendsto g p (𝓝 b)) → TendstoUniformlyOn F (fun _ => b) p s$$
Lean4
/-- If a sequence `g` converges to some `b`, then the sequence of constant functions
`fun n ↦ fun a ↦ g n` converges to the constant function `fun a ↦ b` on any set `s` -/
theorem tendstoUniformlyOn_const {g : ι → β} {b : β} (hg : Tendsto g p (𝓝 b)) (s : Set α) :
TendstoUniformlyOn (fun n : ι => fun _ : α => g n) (fun _ : α => b) p s :=
tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.mpr (hg.tendstoUniformlyOnFilter_const (𝓟 s))
