English
Let f: X → Y be continuous. Then f is specializing if and only if for every x ∈ X, the image f(closure{ x }) is closed in Y.
Русский
Пусть f: X → Y — непрерывное отображение. Тогда f является специализирующим отображением тогда и только тогда, когда образ замыкания {x} в Y замкнут.
LaTeX
$$$\\\\text{SpecializingMap}(f) \\\\iff \\\\forall x \\in X, \\\\ IsClosed( f(\\\\overline{\\\\{x\\\\}}) ).$$$
Lean4
theorem specializingMap_iff_isClosed_image_closure_singleton (hf : Continuous f) :
SpecializingMap f ↔ ∀ x, IsClosed (f '' closure { x }) :=
by
refine
⟨fun h x ↦ ?_, fun h ↦
specializingMap_iff_stableUnderSpecialization_image_singleton.mpr (fun x ↦ (h x).stableUnderSpecialization)⟩
rw [(specializingMap_iff_closure_singleton hf).mp h x]
exact isClosed_closure