English
If f and g tend to atBot along their respective filters, then the product map f,g tends to atBot on the product filter.
Русский
Если f и g сходятся к atBot по соответствующим фильтрам, то отображение Prod.map f g сходится к atBot на произведении фильтров.
LaTeX
$$$\\operatorname{Tendsto} f F \\operatorname{atBot} \\Rightarrow \\operatorname{Tendsto} g G \\operatorname{atBot} \\Rightarrow \\operatorname{Tendsto} (\\operatorname{Prod.map} f g) (F \\times^\\mathrm{S} G) \\operatorname{atBot}$$$
Lean4
theorem prod_atBot [Preorder α] [Preorder γ] {f g : α → γ} (hf : Tendsto f atBot atBot) (hg : Tendsto g atBot atBot) :
Tendsto (Prod.map f g) atBot atBot := by
rw [← prod_atBot_atBot_eq]
exact hf.prod_map_prod_atBot hg
