English
Let f: A → Γ and g: B → Δ be functions, and let a, b be filters on A and B, and c, d be filters on Γ and Δ respectively. If f sends a to c (Tendsto f a c) and g sends b to d (Tendsto g b d), then the product map (a pair map) sends the product filter a × b to c × d; i.e. Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d).
Русский
Пусть f: A → Γ и g: B → Δ — функции, а также фильтры a, b на A и B и фильтры c, d на Γ и Δ соответственно. Если f переводит a в c (Tendsto f a c) и g переводит b в d (Tendsto g b d), то отображение пар (Prod.map f g) переводит произведение фильтров a × b в произведение фильтров c × d; то есть Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d).
LaTeX
$$$ \\operatorname{Tendsto}(\\mathrm{Prod.map}(f,g))\\,(a \\times\\! b)\\,(c \\times\\! d) $$$
Lean4
theorem prodMap {δ : Type*} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β} {c : Filter γ} {d : Filter δ}
(hf : Tendsto f a c) (hg : Tendsto g b d) : Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d) :=
by
rw [Tendsto, Prod.map_def, ← prod_map_map_eq]
exact Filter.prod_mono hf hg
