ι : Type u_2
α : ι → Type u_3
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : Type u_1
m : β → (i : ι) → α i
l : Filter β
⊢ (∀ (i : ι), Tendsto (eval i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)
ι : Type u_2
α : ι → Type u_3
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : Type u_1
m : β → (i : ι) → α i
l : Filter β
⊢ Tendsto m l (pi f) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)
simp only [pi, tendsto_iInf, tendsto_comap_iff]
no goals
ι : Type u_2
α : ι → Type u_3
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : Type u_1
m : β → (i : ι) → α i
l : Filter β
⊢ (∀ (i : ι), Tendsto (eval i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)
rfl