Theorem: TopologySession.Tendsto_iff (HausdorffSchool/Session3_Topology/Tutorial.lean)

State before:
X✝ : Type ?u.2133
Y✝ : Type ?u.2136
X : Type u_1
Y : Type u_2
f : X → Y
F : Filter X
G : Filter Y
⊢ Tendsto f F G ↔ ∀ (S : Set Y), S ∈ G → f ⁻¹' S ∈ F
Tactic:
rfl
State after:
no goals