α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.52575
ι : Sort ?u.52578
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (Filter.prod g g') ↔ Tendsto (fun n => (s n).fst) f g ∧ Tendsto (fun n => (s n).snd) f g'
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.52575
ι : Sort ?u.52578
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (g ×ˢ g') ↔ Tendsto (fun n => (s n).fst) f g ∧ Tendsto (fun n => (s n).snd) f g'
dsimp only [SProd.sprod]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.52575
ι : Sort ?u.52578
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (comap Prod.fst g ⊓ comap Prod.snd g') ↔
    Tendsto (fun n => (s n).fst) f g ∧ Tendsto (fun n => (s n).snd) f g'
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.52575
ι : Sort ?u.52578
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (Filter.prod g g') ↔ Tendsto (fun n => (s n).fst) f g ∧ Tendsto (fun n => (s n).snd) f g'
unfold Filter.prod