mem_closure_image — Mathlib

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

Похожие утверждения