English
If f is continuous at x and x ∈ closure(s), then f(x) ∈ closure(f[s]).
Русский
Если f непрерывна в x и x является точкой в замыкании s, то f(x) лежит в замыкании образа s.
LaTeX
$$$\\text{ContinuousAt}(f,x) \\land x \\in \\overline{s} \\Rightarrow f(x) \\in \\overline{f[s]}$$$
Lean4
theorem mem_closure_image (hf : ContinuousAt f x) (hx : x ∈ closure s) : f x ∈ closure (f '' s) :=
mem_closure_of_frequently_of_tendsto ((mem_closure_iff_frequently.1 hx).mono fun _ => mem_image_of_mem _) hf