prod_map_prod_atTop — Mathlib

English

If f: α → γ tends to atTop along F and g: β → γ tends to atTop along G, then Prod.map f g tends to atTop along the product filter.

Русский

Если f: α → γ стремится к atTop по F, а g: β → γ к atTop по G, то 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_map_prod_atTop [Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ} {g : β → γ} (hf : Tendsto f F atTop)
    (hg : Tendsto g G atTop) : Tendsto (Prod.map f g) (F ×ˢ G) atTop :=
  by
  rw [← prod_atTop_atTop_eq]
  exact hf.prodMap hg

Похожие утверждения