English
A specialization for functions s: α → β × γ: Tendsto s f (g ×ˢ g') is equivalent to Tendsto (fst ∘ s) f g and Tendsto (snd ∘ s) f g'.
Русский
Уточнение для функций s: α → β × γ: Tendsto s f (g × g') эквивалентно Tendsto (fst ∘ s) f g и Tendsto (snd ∘ s) f g'.
LaTeX
$$$ \\operatorname{Tendsto} s f (g \\times\\! g') \\iff \\operatorname{Tendsto} (\\lambda n. (s\,n)^{\\text{fst}}) f g \\wedge \\operatorname{Tendsto} (\\lambda n. (s\,n)^{\\text{snd}}) f g' $$$
Lean4
theorem tendsto_prod_iff' {g' : Filter γ} {s : α → β × γ} :
Tendsto s f (g ×ˢ g') ↔ Tendsto (fun n => (s n).1) f g ∧ Tendsto (fun n => (s n).2) f g' := by
simp only [prod_eq_inf, tendsto_inf, tendsto_comap_iff, Function.comp_def]
