English
If AccPt x F holds and f is continuous at x with f injective, then AccPt f x (map f F).
Русский
Если x является точкой аккумуляции и f непрерывна в окрестности x, и f инъективна, то x переносится в точку аккумуляции f(x) относительно образа фильтра F.
LaTeX
$$$$AccPt x F \rightarrow \forall f,\; ContinuousAt f x \wedge \text{Injective}(f) \Rightarrow AccPt (f x) (\operatorname{map} f F).$$$$
Lean4
theorem map {β : Type*} [TopologicalSpace β] {F : Filter X} {x : X} (h : AccPt x F) {f : X → β} (hf1 : ContinuousAt f x)
(hf2 : Function.Injective f) : AccPt (f x) (map f F) :=
by
apply map_neBot (m := f) (hf := h) |>.mono
rw [Filter.map_inf hf2]
gcongr
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hf1.continuousWithinAt
simpa [hf2.eq_iff] using eventually_mem_nhdsWithin
