no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.317533
ι : Sort x
f : α → β
s : Set α
t : Set β
⊢ Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ (a : α), a ∈ s → f a ∈ t
simp only [tendsto_principal, eventually_principal]