no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.314967
ι : Sort x
f : α → β
x : Filter α
y : ι → Filter β
⊢ Tendsto f x (⨅ (i : ι), y i) ↔ ∀ (i : ι), Tendsto f x (y i)
simp only [Tendsto, iff_self_iff, le_iInf_iff]