English
For a function f: α → β and realizers L1 and L2 for l1 and l2, Tendsto f l1 l2 is equivalent to the usual quantified condition: for every b in L2.σ there exists a in L1.σ such that for all x in L1.F a, f x ∈ L2.F b.
Русский
Для функции f: α → β и реализаторов L1, L2 соответствующих l1 и l2, Tendsto f l1 l2 эквивалентно условию: для каждого b из L2.σ существует a из L1.σ такое, что для всех x ∈ L1.F a, выполняется f x ∈ L2.F b.
LaTeX
$$$\\text{Tendsto}(f,l_1,l_2) \\iff \\forall b, \\exists a, \\forall x \\in L_1.F a, f x \\in L_2.F b$$$
Lean4
theorem tendsto_iff (f : α → β) {l₁ : Filter α} {l₂ : Filter β} (L₁ : l₁.Realizer) (L₂ : l₂.Realizer) :
Tendsto f l₁ l₂ ↔ ∀ b, ∃ a, ∀ x ∈ L₁.F a, f x ∈ L₂.F b :=
(le_iff (L₁.map f) L₂).trans <| forall_congr' fun _ ↦ exists_congr fun _ ↦ image_subset_iff
