English
Under a continuous map f, the image of a generic point is generic for the closure of the image: IsGenericPoint(f(x)) (closure (f''S)).
Русский
При непрерывном отображении f образ обобщенной точки x является обобщенной точкой для замыкания образа: IsGenericPoint(f(x)) (closure (f''S)).
LaTeX
$$$ \mathrm{IsGenericPoint}(x,S) \land \mathrm{Continuous}(f) \Rightarrow \mathrm{IsGenericPoint}(f(x), \overline{f''S})$$$
Lean4
protected theorem image (h : IsGenericPoint x S) {f : α → β} (hf : Continuous f) :
IsGenericPoint (f x) (closure (f '' S)) := by
rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]
