English
If x is a cluster point for lx and f is continuous at x and tends to ly along lx, then f(x) is a cluster point for ly.
Русский
Если x является кластерной точкой относительно lx и f непрерывна в x, а вдоль lx f стремится к ly, то f(x) является кластерной точкой относительно ly.
LaTeX
$$$\\text{ClusterPt}(x, lx) \\rightarrow \\mathrm{ContinuousAt}(f, x) \\rightarrow \\mathrm{Tendsto}(f, lx, ly) \\rightarrow \\text{ClusterPt}(f x, ly)$$$
Lean4
theorem map {lx : Filter X} {ly : Filter Y} (H : ClusterPt x lx) (hfc : ContinuousAt f x) (hf : Tendsto f lx ly) :
ClusterPt (f x) ly :=
(NeBot.map H f).mono <| hfc.tendsto.inf hf
