English
The map p ↦ p.1 × p.2 from Finset ι × Finset ι' to Finset (ι × ι') tends to atTop when domain tends to atTop in each coordinate.
Русский
Отображение p ↦ p.1 × p.2 из пары конечных множеств в произведение ι × ι' стремится к верхнему пределу при стремлении каждого координатного компонента к верхнему пределу.
LaTeX
$$$\\operatorname{Tendsto}\\, (\\lambda p: \\mathrm{Finset}\\, ι \\times \\mathrm{Finset}\\, ι'.\\; p.1 \\times p.2)\\, \\operatorname{atTop}\\, \\operatorname{atTop}$$$
Lean4
theorem tendsto_finset_prod_atTop : Tendsto (fun (p : Finset ι × Finset ι') ↦ p.1 ×ˢ p.2) atTop atTop := by
classical
apply Monotone.tendsto_atTop_atTop
· intro p q hpq
simpa using Finset.product_subset_product hpq.1 hpq.2
· intro b
use (Finset.image Prod.fst b, Finset.image Prod.snd b)
exact Finset.subset_product
