α : Type u_2
β : Type u_3
γ : Type u_4
δ✝ : Type ?u.29553
ι : Sort ?u.29556
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
δ : Type u_1
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map f a ×ˢ map g b ≤ c ×ˢ d
α : Type u_2
β : Type u_3
γ : Type u_4
δ✝ : Type ?u.29553
ι : Sort ?u.29556
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
δ : Type u_1
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)
erw [Tendsto, ← prod_map_map_eq]
no goals
α : Type u_2
β : Type u_3
γ : Type u_4
δ✝ : Type ?u.29553
ι : Sort ?u.29556
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
δ : Type u_1
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map f a ×ˢ map g b ≤ c ×ˢ d
exact Filter.prod_mono hf hg