specializingMap_iff_stableUnderSpecialization_image

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

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