English
If l is a filter on Y, f: Y → ∀ i, A_i tends to x, and g: Y → A_i tends to xi in nhds, then the map a ↦ update (f a) i (g a) tends to update x i xi.
Русский
Если l — фильтр на Y, f: Y → ∀ i A_i сходится к x, а g: Y → A_i сходится к xi в nhds, то a ↦ update(f(a))_i (g(a)) сходится к update(x)_i(xi).
LaTeX
$$$\operatorname{Tendsto} f\ l\ (\mathcal{N} x) \Rightarrow \operatorname{Tendsto} (a \mapsto \operatorname{update}(f(a),i,g(a)))\ l\ (\mathcal{N}(\operatorname{update}(x,i,\xi))).$$$
Lean4
theorem update [DecidableEq ι] {l : Filter Y} {f : Y → ∀ i, A i} {x : ∀ i, A i} (hf : Tendsto f l (𝓝 x)) (i : ι)
{g : Y → A i} {xi : A i} (hg : Tendsto g l (𝓝 xi)) :
Tendsto (fun a => update (f a) i (g a)) l (𝓝 <| update x i xi) :=
tendsto_pi_nhds.2 fun j => by rcases eq_or_ne j i with (rfl | hj) <;> simp [*, hf.apply_nhds]
