English
If k is countably generated, then Tendsto f k l holds if and only if for every sequence x: ℕ → α that tends to k, the composed sequence f ∘ x tends to l.
Русский
Если k счетно порожден, то сходимость f по k к l эквивалентна тому, что для каждой последовательности x: ℕ → α, сходящейся к k, последовательность f ∘ x сходится к l.
LaTeX
$$$\\forall f\\, k\, l, [k.IsCountablyGenerated] :\\n\\operatorname{Tendsto} f\, k\, l \\;\\iff\\; \\forall x:\\mathbb{N} \\to \\alpha, \\operatorname{Tendsto} x\\, atTop\\, k \\;\\Rightarrow\\; \\operatorname{Tendsto}(f \\circ x)\\, atTop\\, l$$$
Lean4
/-- An abstract version of continuity of sequentially continuous functions on metric spaces:
if a filter `k` is countably generated then `Tendsto f k l` iff for every sequence `u`
converging to `k`, `f ∘ u` tends to `l`. -/
theorem tendsto_iff_seq_tendsto {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated] :
Tendsto f k l ↔ ∀ x : ℕ → α, Tendsto x atTop k → Tendsto (f ∘ x) atTop l :=
by
refine ⟨fun h x hx => h.comp hx, fun H s hs => ?_⟩
contrapose! H
have : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ)) := by simpa [neBot_iff, inf_principal_eq_bot]
rcases (k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩
rw [tendsto_inf, tendsto_principal] at hx
refine ⟨x, hx.1, fun h => ?_⟩
rcases (hx.2.and (h hs)).exists with ⟨N, hnotMem, hmem⟩
exact hnotMem hmem
