English
Let f: X → Y be a map between topological spaces. Then f is specializing if and only if the image of every subset of X that is stable under specialization is itself stable under specialization in Y.
Русский
Пусть f: X → Y — отображение между топологическими пространствами. Тогда f является специализирующим отображением тогда и только тогда, когда образ любой подмножества X, сохраняющий специализацию, сохраняет специализацию в Y.
LaTeX
$$$\\\\text{SpecializingMap}(f) \\\\iff \\\\forall S \\subseteq X, \\\\operatorname{StableUnderSpecialization}(S) \\\\to \\\\operatorname{StableUnderSpecialization}(f[S]).$$$
Lean4
theorem specializingMap_iff_stableUnderSpecialization_image :
SpecializingMap f ↔ ∀ s, StableUnderSpecialization s → StableUnderSpecialization (f '' s) :=
Relation.fibration_iff_isLowerSet_image