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