English
Let f: X → Y be a function between topological spaces. Then f is sequentially continuous if for every sequence x_n in X converging to p, the sequence f(x_n) converges to f(p).
Русский
Пусть f: X → Y — отображение между топологическими пространствами. Тогда f последовательностно непрерывна, если для каждой последовательности x_n в X, сходящейся к p, последовательность f(x_n) сходится к f(p).
LaTeX
$$$\\forall x: \\mathbb{N} \\to X, \\forall p \\in X, \\operatorname{Tendsto} x\\,\\text{atTop} (\\mathcal{N} p)\\;\\Rightarrow\\; \\operatorname{Tendsto} (f \\circ x) \\text{atTop} (\\mathcal{N} (f p))$$$
Lean4
/-- A function between topological spaces is sequentially continuous if it commutes with limit of
convergent sequences. -/
def SeqContinuous (f : X → Y) : Prop :=
∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, Tendsto x atTop (𝓝 p) → Tendsto (f ∘ x) atTop (𝓝 (f p))
