prod_map_prod_atBot — Mathlib

English

If f: α → γ tends to atBot along F and g: β → γ tends to atBot along G, then Prod.map f g tends to atBot along F ×ˢ G.

Русский

Если f: α → γ сходится к atBot вдоль F, а g: β → γ сходится к atBot вдоль G, то отображение Prod.map f g сходится к atBot вдоль F ×ˢ G.

LaTeX

$$$\\operatorname{Tendsto} (\\operatorname{Prod.map} f g) (F \\times^\\mathrm{S} G) \\operatorname{atBot}$$$

Lean4

theorem prod_map_prod_atBot [Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ} {g : β → γ} (hf : Tendsto f F atBot)
    (hg : Tendsto g G atBot) : Tendsto (Prod.map f g) (F ×ˢ G) atBot :=
  by
  rw [← prod_atBot_atBot_eq]
  exact hf.prodMap hg

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